Commit 2023-11-21 08:44 81e04e35

View on Github →

feat(CategoryTheory): the regular topology is subcanonical (#8529) We prove that the regular topology on any Preregular category is subcanonical.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent.lean

deleted theorem CategoryTheory.coherentTopology.isSubcanonical

added theorem CategoryTheory.coherentTopology.subcanonical

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

deleted theorem CategoryTheory.EqualizerCondition.isSheafFor

deleted theorem CategoryTheory.EqualizerCondition.isSheaf_iff

deleted def CategoryTheory.EqualizerCondition

deleted def CategoryTheory.MapToEqualizer

deleted theorem CategoryTheory.equalizerCondition_of_regular

deleted theorem CategoryTheory.isSheafFor_regular_of_projective

deleted theorem CategoryTheory.isSheaf_of_projective

added theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheafFor

added theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheaf_iff

added def CategoryTheory.regularCoverage.EqualizerCondition

added def CategoryTheory.regularCoverage.MapToEqualizer

added theorem CategoryTheory.regularCoverage.equalizerCondition_of_regular

added theorem CategoryTheory.regularCoverage.isSheafFor_regular_of_projective

added theorem CategoryTheory.regularCoverage.isSheaf_of_projective

added theorem CategoryTheory.regularCoverage.isSheaf_yoneda_obj

added theorem CategoryTheory.regularCoverage.subcanonical