Commit 2025-05-16 18:32 9bdfd589

View on Github →

chore(AlgebraicGeometry): golf file with ideal sheaf API (#24762)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

deleted def AlgebraicGeometry.affineTargetImage

deleted def AlgebraicGeometry.affineTargetImageFactorization

deleted theorem AlgebraicGeometry.affineTargetImageFactorization_app_injective

deleted theorem AlgebraicGeometry.affineTargetImageFactorization_comp

deleted def AlgebraicGeometry.affineTargetImageInclusion

deleted theorem AlgebraicGeometry.affineTargetImageInclusion_app_surjective

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added theorem AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso

added theorem AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal

deleted theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_iSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_sSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top

added theorem AlgebraicGeometry.Scheme.nilradical_eq_bot

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added theorem AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot

added theorem AlgebraicGeometry.isDominant_of_of_appTop_injective

deleted theorem AlgebraicGeometry.surjective_of_isClosed_range_of_injective

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.isRadical_bot

added theorem Ideal.isRadical_bot_iff