Commit 2025-05-12 15:20 85ff0a1d

View on Github →

chore(AlgebraicGeometry): split IdealSheaf.lean (#24759) Surprisingly, I managed to develop some more API for ideal sheaves that needs to import IsClosedImmersion.lean and live in a different file, so we might as well create a folder and split the 1400+ line file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp

deleted theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply

deleted theorem AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp

deleted theorem AlgebraicGeometry.Scheme.Hom.ideal_ker_le

deleted def AlgebraicGeometry.Scheme.Hom.ker

deleted theorem AlgebraicGeometry.Scheme.Hom.ker_apply

deleted theorem AlgebraicGeometry.Scheme.Hom.le_ker_comp

deleted theorem AlgebraicGeometry.Scheme.Hom.range_subset_ker_support

deleted theorem AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective

deleted theorem AlgebraicGeometry.Scheme.Hom.support_ker

deleted def AlgebraicGeometry.Scheme.Hom.toImage

deleted def AlgebraicGeometry.Scheme.Hom.toImageAux

deleted theorem AlgebraicGeometry.Scheme.Hom.toImage_app

deleted theorem AlgebraicGeometry.Scheme.Hom.toImage_app_injective

deleted theorem AlgebraicGeometry.Scheme.Hom.toImage_imageι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical

deleted def AlgebraicGeometry.Scheme.IdealSheafData.Simps.coe_support

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter

deleted def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.gc

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueData

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjCarrierIso

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_id

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι

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

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux

deleted def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT

deleted def AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo

deleted def AlgebraicGeometry.Scheme.IdealSheafData.gluedTo

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_top

deleted def AlgebraicGeometry.Scheme.IdealSheafData.inclusion

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.le_def

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.le_radical

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal'

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem

deleted def AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff

deleted def AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop

deleted def AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map

deleted def AlgebraicGeometry.Scheme.IdealSheafData.radical

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_bot

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_inf

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_sup

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_top

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι

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

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

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subscheme

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subschemeIso

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso

deleted def AlgebraicGeometry.Scheme.IdealSheafData.subschemeι

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal

deleted def AlgebraicGeometry.Scheme.IdealSheafData.support

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_antitone

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_bot

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_radical

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_top

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet

deleted structure AlgebraicGeometry.Scheme.IdealSheafData

deleted theorem AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp

deleted def AlgebraicGeometry.Scheme.kerAdjunction

deleted def AlgebraicGeometry.Scheme.kerFunctor

deleted theorem AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty

deleted theorem AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion

deleted theorem AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal

deleted theorem AlgebraicGeometry.Scheme.ker_of_isAffine

deleted def AlgebraicGeometry.Scheme.nilradical

deleted theorem AlgebraicGeometry.Scheme.support_nilradical

Created Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp

added theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply

added theorem AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp

added theorem AlgebraicGeometry.Scheme.Hom.ideal_ker_le

added def AlgebraicGeometry.Scheme.Hom.ker

added theorem AlgebraicGeometry.Scheme.Hom.ker_apply

added theorem AlgebraicGeometry.Scheme.Hom.le_ker_comp

added theorem AlgebraicGeometry.Scheme.Hom.range_subset_ker_support

added theorem AlgebraicGeometry.Scheme.Hom.support_ker

added theorem AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical

added def AlgebraicGeometry.Scheme.IdealSheafData.Simps.coe_support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus

added theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter

added def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine

added theorem AlgebraicGeometry.Scheme.IdealSheafData.gc

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_def

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_radical

added theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal'

added theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem

added def AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff

added def AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop

added def AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono

added def AlgebraicGeometry.Scheme.IdealSheafData.radical

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_inf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal

added def AlgebraicGeometry.Scheme.IdealSheafData.support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter

added theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_antitone

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_radical

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet

added structure AlgebraicGeometry.Scheme.IdealSheafData

added def AlgebraicGeometry.Scheme.kerFunctor

added theorem AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty

added theorem AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion

added theorem AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal

added theorem AlgebraicGeometry.Scheme.ker_of_isAffine

added def AlgebraicGeometry.Scheme.nilradical

added theorem AlgebraicGeometry.Scheme.support_nilradical

Created Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

added theorem AlgebraicGeometry.Scheme.IdealSheafData.Hom.stalkFunctor_toImage_injective

added def AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImage

added def AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImageAux

added theorem AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImage_app

added theorem AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImage_app_injective

added theorem AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImage_imageι

added def AlgebraicGeometry.Scheme.IdealSheafData.glueData

added def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj

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

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 def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT

added def AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo

added def AlgebraicGeometry.Scheme.IdealSheafData.gluedTo

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_ker_le_ker_ΓSpecIso_inv_comp

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι

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.isLocalization_away

added def AlgebraicGeometry.Scheme.IdealSheafData.kerAdjunction

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app

added theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap

added theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map

added theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι

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

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.subschemeFunctor

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ι_app_surjective

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean