Theorem CategoryTheory.regularCoverage.isSheaf_of_projective

Modification history

2024-04-03 20:13
Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
feat(CategoryTheory/Sites): add some API for regular sheaves and the equalizer condition (#10420) …
Deleted CategoryTheory.regularCoverage.isSheaf_of_projectiveView on Github →
2024-02-10 10:41
Mathlib/CategoryTheory/Sites/Coherent/RegularExtensive.lean
chore(CategoryTheory/Sites): reorganise the material related to the coherent, regular and extensive topologies (#9944) …
Modified CategoryTheory.regularCoverage.isSheaf_of_projectiveView on Github →
2024-01-16 02:11
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
chore(CategoryTheory/Sites): universe polymorphic `EqualizerCondition` (#9729) …
Modified CategoryTheory.regularCoverage.isSheaf_of_projectiveView on Github →
2023-11-21 08:44
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat(CategoryTheory): the regular topology is subcanonical (#8529) …
Added CategoryTheory.regularCoverage.isSheaf_of_projectiveView on Github →