Skip to content

[Merged by Bors] - feat(CategoryTheory): characterise the covering sieves for the extensive topology#13897

Closed
dagurtomas wants to merge 59 commits intomasterfrom
dagur/ExtensiveTopologySieves
Closed

[Merged by Bors] - feat(CategoryTheory): characterise the covering sieves for the extensive topology#13897
dagurtomas wants to merge 59 commits intomasterfrom
dagur/ExtensiveTopologySieves

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jun 17, 2024

Open in Gitpod

joelriou and others added 30 commits March 27, 2024 10:10
@joelriou
feat: morphisms of presheaves that are locally injective for a Grothe…
c5b2eb7 
…ndieck topology
@joelriou
fixing Mathlib.lean
b1e30a8
@joelriou
Merge remote-tracking branch 'origin' into localy-injective
f13e658
@joelriou
Merge remote-tracking branch 'origin' into localy-injective
a7ee7f1
@joelriou
fixing the build
0b6ec5d
@joelriou
Merge remote-tracking branch 'origin' into localy-injective
84668f5
@joelriou
isLocallyInjective_forget_iff
e40fc47
@joelriou
isLocallyInjective_iff_equalizerSieve_mem_imp
0d3bf2f
@joelriou @erdOne
Update Mathlib/CategoryTheory/Sites/LocallyInjective.lean
bb68433 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@joelriou
removed IsSeparated
4c7a25b
@joelriou
Merge remote-tracking branch 'origin' into localy-injective
5b374a4
@joelriou
Merge remote-tracking branch 'origin' into localy-injective
6b0510c
@joelriou
added code by @erdOne
7deb0c5
@joelriou
feat(CategoryTheory/Sites): more properties of locally surjective mor…
e4b68dd 
…phisms of presheaves
@joelriou
fixing the build
a1b80fd
@joelriou
fixing the build
d1bef11
@joelriou
feat(CategoryTheory/Sites): locally bijective morphisms of presheaves
6054187
@joelriou
removed sorries
6842290
@joelriou
cleaning up
c6c26dd
@joelriou
Merge remote-tracking branch 'origin' into locally-surjective-extra
d985f5f
@joelriou
Merge remote-tracking branch 'origin/locally-surjective-extra' into l…
e683715 
…ocally-bijective
@joelriou
feat(CategoryTheory/MorphismProperty): the factorization axiom
e6e87ce
@joelriou
added functorCategory
6886cdb
@joelriou
added comp and comp_eq_top_iff
662286f
@joelriou
Merge remote-tracking branch 'origin' into factorization-axiom
b09399d
@joelriou
Merge remote-tracking branch 'origin' into locally-bijective
e2c0345
@joelriou
feat(CategoryTheory): surjective-injective factorizations in concrete…
4e77ebb 
… categories
@joelriou
typo
2493941
@joelriou
Merge remote-tracking branch 'origin/locally-bijective' into locally-…
64c3b41 
…surjective-iff-epi
@joelriou
feat(CategoryTheory/Sites): epi-mono factorization for sheaves
b2fc7b6
@github-actions
Copy link
Copy Markdown

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

PR summary 526a38e788

Import changes

No significant changes to the import graph

Declarations diff

+ Cofan.isColimitTrans
+ Cofan.isColimit_iff_isIso_sigmaDesc
+ coherentExtensiveEquivalence
+ extensiveTopology.mem_sieves_iff_contains_colimit_cofan
+ instance (F : Sheaf (extensiveTopology C) D) : PreservesFiniteProducts F.val
+ instance [Preregular C] [FinitaryExtensive C]
+ isSheaf_iff_extensiveSheaf_of_projective

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>

dagurtomas
dagurtomas commented Jun 17, 2024
View reviewed changes
This was referenced Jun 17, 2024
Closed
Closed
@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory labels Jun 17, 2024
@riccardobrasca riccardobrasca self-assigned this Jun 17, 2024
riccardobrasca
riccardobrasca reviewed Jun 17, 2024
View reviewed changes
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 17, 2024
riccardobrasca
riccardobrasca reviewed Jun 17, 2024
View reviewed changes
riccardobrasca
riccardobrasca reviewed Jun 17, 2024
View reviewed changes
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jun 17, 2024

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 17, 2024

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 17, 2024
dagurtomas and others added 3 commits June 17, 2024 15:59
@dagurtomas @riccardobrasca
Update Mathlib/CategoryTheory/Limits/Shapes/Products.lean
13b8bf9 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@dagurtomas @riccardobrasca
Update Mathlib/CategoryTheory/Limits/Shapes/Products.lean
64d7a26 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@dagurtomas
clean up the extensive sheaves file
526a38e
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Jun 17, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 17, 2024
@joelriou @dagurtomas
feat(CategoryTheory): characterise the covering sieves for the extens…
402ae16 
…ive topology (#13897)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): characterise the covering sieves for the extensive topology [Merged by Bors] - feat(CategoryTheory): characterise the covering sieves for the extensive topology Jun 17, 2024
@mathlib-bors mathlib-bors bot closed this Jun 17, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/ExtensiveTopologySieves branch June 17, 2024 14:41
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@joelriou @dagurtomas @AntoineChambert-Loir
feat(CategoryTheory): characterise the covering sieves for the extens…
73672a3 
…ive topology (#13897)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@joelriou @dagurtomas @kbuzzard
feat(CategoryTheory): characterise the covering sieves for the extens…
ae1f72d 
…ive topology (#13897)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees

@riccardobrasca riccardobrasca

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@dagurtomas @riccardobrasca @joelriou