Commit 2025-05-10 07:53 572abed1

View on Github →

feat(AlgebraicGeometry): equivalence between ideal sheaves and closed subschemes (#24615)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

added theorem AlgebraicGeometry.Scheme.Hom.ideal_ker_le

added theorem AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective

added def AlgebraicGeometry.Scheme.Hom.toImage

added def AlgebraicGeometry.Scheme.Hom.toImageAux

added theorem AlgebraicGeometry.Scheme.Hom.toImage_app

added theorem AlgebraicGeometry.Scheme.Hom.toImage_app_injective

added theorem AlgebraicGeometry.Scheme.Hom.toImage_imageι

added def AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective

added theorem AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp

added def AlgebraicGeometry.Scheme.kerAdjunction

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

added def AlgebraicGeometry.IsClosedImmersion.lift

added theorem AlgebraicGeometry.IsClosedImmersion.lift_fac

added def AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.IsBasis.of_isInducing

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.germ_eq_of_isBasis

added theorem TopCat.Presheaf.germ_exist_of_isBasis

modified theorem TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective

added theorem TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis