Commit 2023-10-20 14:35 0227fee3

View on Github →

feat: description of sheaves for regular sieves (#6919) We prove that presheaves satisfying an equaliser condition on preregular categories are sheaves for regular presieves.

depends on: #6876

Estimated changes

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

added theorem CategoryTheory.EqualizerCondition.isSheafFor

added def CategoryTheory.EqualizerCondition

added def CategoryTheory.EqualizerFirstObjIso

added def CategoryTheory.EqualizerSecondObjIso

added theorem CategoryTheory.IsSheafForRegular.equalizerCondition

added def CategoryTheory.MapToEqualizer

added theorem CategoryTheory.isSheafFor_regular_of_projective

added theorem CategoryTheory.isSheaf_iff_equalizerCondition

added theorem CategoryTheory.isSheaf_of_projective