Commit 2025-04-22 18:08 a29b84dc

View on Github →

refactor(AlgebraicGeometry): add supportSet field to IdealSheafData (#23890)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

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

modified def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.gc

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_top

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem

added def AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff

modified def AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop

modified def AlgebraicGeometry.Scheme.IdealSheafData.radical

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal

modified def AlgebraicGeometry.Scheme.IdealSheafData.support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter

added theorem AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.support_antitone

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.support_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_empty_iff

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_inter

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_ofIdealTop

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_radical

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_subset_zeroLocus

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.support_top

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.support_vanishingIdeal

modified theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet

added theorem AlgebraicGeometry.Scheme.support_nilradical

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.zeroLocus_radical