Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-11 22:37
6b5c9028
View on Github →
feat: port CategoryTheory.Sites.CoverLifting (
#3898
) Mostly straightforward.
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Sites/CoverLifting.lean
added
structure
CategoryTheory.CoverLifting
added
def
CategoryTheory.RanIsSheafOfCoverLifting.getSection
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.getSection_commute
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.getSection_isAmalgamation
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.getSection_is_unique
added
def
CategoryTheory.RanIsSheafOfCoverLifting.gluedLimitCone
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.gluedLimitCone_π_app
added
def
CategoryTheory.RanIsSheafOfCoverLifting.gluedSection
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.gluedSection_isAmalgamation
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.gluedSection_is_unique
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.helper
added
def
CategoryTheory.RanIsSheafOfCoverLifting.pulledbackFamily
added
theorem
CategoryTheory.RanIsSheafOfCoverLifting.pulledbackFamily_apply
added
def
CategoryTheory.Sites.copullback
added
theorem
CategoryTheory.compCoverLifting
added
theorem
CategoryTheory.idCoverLifting
added
theorem
CategoryTheory.ran_isSheaf_of_coverLifting