Commit 2025-02-04 06:23 62d4aefe

View on Github →

feat(AlgebraicGeometry): ideal sheaf data on a scheme (#21052)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.ideal_ext_iff

added theorem AlgebraicGeometry.IsAffineOpen.ideal_le_iff

added theorem AlgebraicGeometry.IsAffineOpen.mem_ideal_iff

added theorem AlgebraicGeometry.Scheme.affineBasicOpen_le

Created Mathlib/AlgebraicGeometry/IdealSheaf.lean

added def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine

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_support

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.map_ideal'

added theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem

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 theorem AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal

added def AlgebraicGeometry.Scheme.IdealSheafData.support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_antitone

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_empty_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_inter

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_ofIdealTop

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_subset_zeroLocus

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_support

added structure AlgebraicGeometry.Scheme.IdealSheafData

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.map_radical