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