Commit 2025-03-10 20:54 c4b22380

View on Github →

feat(AlgebraicGeometry): constructor for IsColimit (Cofan.mk S f) (#22541) Also generalizes some universe assumptions in Mathlib.AlgebraicGeometry.Limits.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

modified theorem AlgebraicGeometry.exists_sigmaι_eq

modified theorem AlgebraicGeometry.isOpenImmersion_sigmaDesc

added theorem AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl

added theorem AlgebraicGeometry.nonempty_isColimit_cofanMk_of

modified def AlgebraicGeometry.sigmaOpenCover

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

added theorem AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top

Modified Mathlib/Data/Opposite.lean

added theorem Opposite.small

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

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean