Commit 2025-06-13 16:09 25f8b1a9

View on Github →

feat(AlgebraicGeometry): locally directed gluing (#24796)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Cover/Sigma.lean

Modified Mathlib/AlgebraicGeometry/Gluing.lean

added def AlgebraicGeometry.Scheme.IsLocallyDirected.V

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.V_self

added def AlgebraicGeometry.Scheme.IsLocallyDirected.cocone

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv

added def AlgebraicGeometry.Scheme.IsLocallyDirected.glueData

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux

added def AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit

added def AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace

added def AlgebraicGeometry.Scheme.IsLocallyDirected.openCover

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_J

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_map

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_obj

added def AlgebraicGeometry.Scheme.IsLocallyDirected.t

added def AlgebraicGeometry.Scheme.IsLocallyDirected.tAux

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.t_id

added theorem AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff

added theorem AlgebraicGeometry.Scheme.hom_ext_of_forall

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

deleted def AlgebraicGeometry.disjointGlueData'

deleted def AlgebraicGeometry.disjointGlueData

deleted theorem AlgebraicGeometry.exists_sigmaι_eq

deleted theorem AlgebraicGeometry.iSup_opensRange_sigmaι

deleted def AlgebraicGeometry.sigmaIsoGlued

deleted def AlgebraicGeometry.sigmaOpenCover

deleted def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofan

deleted def AlgebraicGeometry.toLocallyRingedSpaceCoproductCofanIsColimit

deleted theorem AlgebraicGeometry.ι_sigmaIsoGlued_hom

deleted theorem AlgebraicGeometry.ι_sigmaIsoGlued_inv

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.comp_lift

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added def AlgebraicGeometry.Scheme.Opens.iSupOpenCover

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.forget_map

added theorem AlgebraicGeometry.Scheme.forget_obj

Created Mathlib/CategoryTheory/LocallyDirected.lean