Commit 2026-01-16 12:21 2b4c6152

View on Github →

feat(AlgebraicGeometry): Scheme has disjoint coproducts (#34014) From Proetale.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

modified theorem AlgebraicGeometry.disjoint_opensRange_sigmaι

added theorem AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne

added theorem AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne

added theorem AlgebraicGeometry.isInitial_iff_isEmpty

modified theorem AlgebraicGeometry.sigmaι_eq_iff

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

added theorem CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct