Commit 2025-04-22 10:51 9b8d0f15

View on Github →

chore: generalize universes for (pre)sheaves of types (#22824)

Estimated changes

Modified Mathlib/CategoryTheory/Category/Pairwise.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

added def TopCat.LocalPredicate.and

added def TopCat.PrelocalPredicate.and

modified def TopCat.PrelocalPredicate.sheafify

modified theorem TopCat.PrelocalPredicate.sheafifyOf

modified def TopCat.continuousLocal

modified def TopCat.continuousPrelocal

added def TopCat.isSection

modified def TopCat.sheafToTop

modified def TopCat.subpresheafContinuousPrelocalIsoPresheafToTop

modified def TopCat.subpresheafToTypes

modified def TopCat.subsheafToTypes

Modified Mathlib/Topology/Sheaves/PresheafOfFunctions.lean

modified def TopCat.presheafToTop

modified theorem TopCat.presheafToTop_obj

modified def TopCat.presheafToType

modified theorem TopCat.presheafToType_map

modified theorem TopCat.presheafToType_obj

modified def TopCat.presheafToTypes

modified theorem TopCat.presheafToTypes_map

modified theorem TopCat.presheafToTypes_obj

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

added theorem TopCat.Presheaf.IsSheaf.isSheafOpensLeCover

Modified Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean

added theorem TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections

added theorem TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections

added def TopCat.Presheaf.isLimitOpensLeCoverEquivPairwise

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

added theorem TopCat.Presheaf.IsSheaf.isSheafUniqueGluing

added theorem TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types

Modified Mathlib/Topology/Sheaves/SheafOfFunctions.lean

modified theorem TopCat.Presheaf.toType_isSheaf

modified theorem TopCat.Presheaf.toTypes_isSheaf

modified def TopCat.sheafToType

modified def TopCat.sheafToTypes