Commit 2024-07-15 20:56 2df4be31

View on Github →

feat(AlgebraicGeometry/Limits): Coproducts of Schemes (#14429)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

added def AlgebraicGeometry.disjointGlueData'

added def AlgebraicGeometry.disjointGlueData

added theorem AlgebraicGeometry.disjoint_opensRange_sigmaι

added theorem AlgebraicGeometry.exists_sigmaι_eq

added theorem AlgebraicGeometry.iSup_opensRange_sigmaι

added def AlgebraicGeometry.sigmaIsoGlued

added def AlgebraicGeometry.sigmaMk

added theorem AlgebraicGeometry.sigmaMk_mk

added def AlgebraicGeometry.sigmaOpenCover

added theorem AlgebraicGeometry.sigmaι_eq_iff

added def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofan

added def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofanIsColimit

added theorem AlgebraicGeometry.ι_sigmaIsoGlued_hom

added theorem AlgebraicGeometry.ι_sigmaIsoGlued_inv

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.IsOpenImmersion.of_isLocalization