[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules #13478

dagurtomas · 2024-06-03T11:02:37Z

This PR characterises epimorphisms in condensed sets and condensed R-modules for any ring R, as morphisms of sheaves which are objectwise surjective on Stonean.

depends on: [Merged by Bors] - feat(CategoryTheory): characterise the covering sieves for the extensive topology #13897
depends on: [Merged by Bors] - feat(CategoryTheory): characterise locally surjective morphisms in categories of coherent/regular/extensive sheaves #13898

…ndieck topology

Co-authored-by: Andrew Yang <[email protected]>

…phisms of presheaves

…ocally-bijective

… categories

…surjective-iff-epi

github-actions · 2024-06-17T13:29:59Z

PR summary c6b1833b88

Import changes

No significant changes to the import graph

Declarations diff

+++ epi_iff_locallySurjective_on_compHaus
+++ epi_iff_surjective_on_stonean

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean

leanprover-community-mathlib4-bot · 2024-07-01T10:47:13Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory): characterise the covering sieves for the extensive topology #13897~~
~~[Merged by Bors] - feat(CategoryTheory): characterise locally surjective morphisms in categories of coherent/regular/extensive sheaves #13898~~
By Dependent Issues (🤖). Happy coding!

joelriou · 2024-07-10T16:45:35Z

Thanks!

bors merge

…les (#13478) This PR characterises epimorphisms in condensed sets and condensed `R`-modules for any ring `R`, as morphisms of sheaves which are objectwise surjective on `Stonean`. Co-authored-by: Joël Riou <[email protected]> Co-authored-by: dagurtomas <[email protected]> Co-authored-by: Dagur Tómas Ásgeirsson <[email protected]>

mathlib-bors · 2024-07-10T18:10:29Z

Pull request successfully merged into master.

Build succeeded:

joelriou and others added 30 commits March 27, 2024 10:10

feat: morphisms of presheaves that are locally injective for a Grothe…

c5b2eb7

…ndieck topology

fixing Mathlib.lean

b1e30a8

Merge remote-tracking branch 'origin' into localy-injective

f13e658

Merge remote-tracking branch 'origin' into localy-injective

a7ee7f1

fixing the build

0b6ec5d

Merge remote-tracking branch 'origin' into localy-injective

84668f5

isLocallyInjective_forget_iff

e40fc47

isLocallyInjective_iff_equalizerSieve_mem_imp

0d3bf2f

Update Mathlib/CategoryTheory/Sites/LocallyInjective.lean

bb68433

Co-authored-by: Andrew Yang <[email protected]>

removed IsSeparated

4c7a25b

Merge remote-tracking branch 'origin' into localy-injective

5b374a4

Merge remote-tracking branch 'origin' into localy-injective

6b0510c

added code by @erdOne

7deb0c5

feat(CategoryTheory/Sites): more properties of locally surjective mor…

e4b68dd

…phisms of presheaves

fixing the build

a1b80fd

fixing the build

d1bef11

feat(CategoryTheory/Sites): locally bijective morphisms of presheaves

6054187

removed sorries

6842290

cleaning up

c6c26dd

Merge remote-tracking branch 'origin' into locally-surjective-extra

d985f5f

Merge remote-tracking branch 'origin/locally-surjective-extra' into l…

e683715

…ocally-bijective

feat(CategoryTheory/MorphismProperty): the factorization axiom

e6e87ce

added functorCategory

6886cdb

added comp and comp_eq_top_iff

662286f

Merge remote-tracking branch 'origin' into factorization-axiom

b09399d

Merge remote-tracking branch 'origin' into locally-bijective

e2c0345

feat(CategoryTheory): surjective-injective factorizations in concrete…

4e77ebb

… categories

typo

2493941

Merge remote-tracking branch 'origin/locally-bijective' into locally-…

64c3b41

…surjective-iff-epi

feat(CategoryTheory/Sites): epi-mono factorization for sheaves

b2fc7b6

dagurtomas added awaiting-review awaiting-CI labels Jun 3, 2024

github-actions bot removed the awaiting-CI label Jun 3, 2024

dagurtomas added 3 commits June 3, 2024 16:15

rw -> erw

806f188

erw -> rw

b188403

erw -> rw

24fa6ac

dagurtomas mentioned this pull request Jun 4, 2024

[Merged by Bors] - feat(LightCondensed): characterise epimorphisms in light condensed sets and modules #13495

Closed

2 tasks

Merge branch 'master' into dagur/CondensedEpi

efec126

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 17, 2024

dagurtomas commented Jun 17, 2024

View reviewed changes

Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean Outdated Show resolved Hide resolved

Update Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean

6502346

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 17, 2024

Merge branch 'master' into dagur/CondensedEpi

5ade817

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 17, 2024

dagurtomas mentioned this pull request Jun 17, 2024

[Merged by Bors] - feat(CategoryTheory): characterise locally surjective morphisms in categories of coherent/regular/extensive sheaves #13898

Closed

1 task

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 1, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024

Merge branch 'master' into dagur/CondensedEpi

c6b1833

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024

kim-em removed the awaiting-review label Jul 9, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 10, 2024

mathlib-bors bot changed the title ~~feat(Condensed): characterise epimorphisms in condensed sets and modules~~ [Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules Jul 10, 2024

mathlib-bors bot closed this Jul 10, 2024

mathlib-bors bot deleted the dagur/CondensedEpi branch July 10, 2024 18:10

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules #13478

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules #13478

dagurtomas commented Jun 3, 2024 •

edited by github-actions bot

Loading

github-actions bot commented Jun 17, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Jul 1, 2024

joelriou commented Jul 10, 2024

mathlib-bors bot commented Jul 10, 2024

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules #13478

[Merged by Bors] - feat(Condensed): characterise epimorphisms in condensed sets and modules #13478

Conversation

dagurtomas commented Jun 3, 2024 • edited by github-actions bot Loading

github-actions bot commented Jun 17, 2024 • edited Loading

PR summary c6b1833b88

Import changes

Declarations diff

leanprover-community-mathlib4-bot commented Jul 1, 2024

joelriou commented Jul 10, 2024

mathlib-bors bot commented Jul 10, 2024

dagurtomas commented Jun 3, 2024 •

edited by github-actions bot

Loading

github-actions bot commented Jun 17, 2024 •

edited

Loading