Commit 2025-06-15 07:29 0905ae82

View on Github →

chore(CategoryTheory/Sites): generalize universes for sheafification (#25877)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

modified theorem CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit

Modified Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

modified def CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation

modified def CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux

modified theorem CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac

modified def CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj

modified theorem CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac

Modified Mathlib/CategoryTheory/Sites/Plus.lean

Modified Mathlib/Condensed/Discrete/Module.lean