Commit 2025-02-18 17:29 167dee15

View on Github →

feat(AlgebraicGeometry): closed subscheme of an ideal sheaf (#21951) We only construct the glue data in this PR. In follow up PRs we will give it the right underlying set and prove various properties about it.

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

added def AlgebraicGeometry.Scheme.IdealSheafData.glueData

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop

added theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap

added theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.Scheme.Hom.isIso_app

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.RingHom.ker_comp_of_injective

modified theorem Ideal.RingHom.ker_equiv

added theorem Ideal.RingHom.ker_equiv_comp

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.of_surjective