Commit 2025-05-05 12:18 98534d59

View on Github →

feat(AlgebraicGeometry): subscheme associated to an ideal sheaf (#23513)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjCarrierIso

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_id

added theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst

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

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd

added def AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo

added def AlgebraicGeometry.Scheme.IdealSheafData.gluedTo

added def AlgebraicGeometry.Scheme.IdealSheafData.inclusion

added theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp

added theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id

added theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app

added theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map

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

added theorem AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion

added def AlgebraicGeometry.Scheme.IdealSheafData.subscheme

added def AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι

added def AlgebraicGeometry.Scheme.IdealSheafData.subschemeIso

added def AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso

added def AlgebraicGeometry.Scheme.IdealSheafData.subschemeι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply

added def AlgebraicGeometry.Scheme.kerFunctor

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added def AlgebraicGeometry.Scheme.Hom.copyBase

added theorem AlgebraicGeometry.Scheme.Hom.copyBase_eq

added theorem AlgebraicGeometry.Scheme.coe_homeoOfIso

added theorem AlgebraicGeometry.Scheme.coe_homeoOfIso_symm