Commit 2025-03-05 21:20 696a735b

View on Github →

chore(Geometry/RingedSpace): generalize universe assumptions for limits and colimits (#22543)

Estimated changes

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

modified theorem AlgebraicGeometry.SheafedSpace.colimit_exists_rep

modified theorem AlgebraicGeometry.SheafedSpace.isColimit_exists_rep

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/Topology/Sheaves/Limits.lean

modified theorem TopCat.isSheaf_of_isLimit

modified theorem TopCat.limit_isSheaf