The stalk of a closed subscheme is the quotient of the stalk by the stalk ideal

For an ideal sheaf Z on a scheme X with closed subscheme ι : V(Z) ⟶ X and a point z ∈ V(Z) over x = ι z, the stalk map ι^♯_z : 𝒪_{X,x} → 𝒪_{V(Z),z} is surjective (a closed immersion) with kernel the stalk Z_x = stalkIdeal Z x of the ideal sheaf, so 𝒪_{V(Z),z} ≅ 𝒪_{X,x}/Z_x (stalkQuotientEquiv) and the residue fields agree (residueFieldStalkEquiv). This is the identification 𝒪_{Z,x} = 𝒪_{X,x}/I_x, Kollár's "the local ring of Z at x", used without comment throughout the sources.

Proof of the kernel formula (the local form of [TSPA, Tags 01HP, 01QN]): on an affine open U ∋ x the stalk 𝒪_{X,x} is the localization Γ(X, U)_𝔭 and 𝒪_{V(Z),z} is the localization of Γ(V(Z), ι⁻¹U) = Γ(X, U)/Z(U) at the corresponding prime 𝔮; the stalk map is the localization of the surjection Γ(X, U) → Γ(X, U)/Z(U) (Mathlib's ker_subschemeι_app, subschemeι_app_surjective, comap_primeIdealOf_appLE), and the kernel of a localized map is the localization of the kernel (IsLocalization.ker_map), which is Z(U)·𝒪_{X,x} = Z_x (stalkIdeal_eq_map_germ).

Used wherever the local ring of a closed subscheme is computed from that of the ambient scheme (Hironaka/Scheme/Smooth/AdaptedCoordinates.lean, Hironaka/Snc/, Hironaka/Sequence/, Hironaka/Resolution/).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_subschemeι_eq {X : Scheme} (Z : X.IdealSheafData) {x : ↥X} (hx : x ∈ Z.support) : ∃ (z : ↥Z.subscheme), Z.subschemeι z = x

A point of the support of Z is the image of a point of the closed subscheme V(Z).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_stalkMap_subschemeι {X : Scheme} (Z : X.IdealSheafData) (z : ↥Z.subscheme) : RingHom.ker (CommRingCat.Hom.hom (Hom.stalkMap Z.subschemeι z)) = Z.stalkIdeal (Z.subschemeι z)

The kernel of the stalk map of the closed immersion V(Z) ⟶ X at z is the stalk of Z at ι z.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.stalkQuotientEquiv {X : Scheme} (Z : X.IdealSheafData) (z : ↥Z.subscheme) : ↑(X.presheaf.stalk (Z.subschemeι z)) ⧸ Z.stalkIdeal (Z.subschemeι z) ≃+* ↑(Z.subscheme.presheaf.stalk z)

𝒪_{V(Z),z} ≅ 𝒪_{X,ι z} / Z_{ι z}: the stalk of the closed subscheme is the quotient of the stalk of X by the stalk of the ideal sheaf.

Equations

• Z.stalkQuotientEquiv z = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkQuotientEquiv_mk {X : Scheme} (Z : X.IdealSheafData) (z : ↥Z.subscheme) (a : ↑(X.presheaf.stalk (Z.subschemeι z))) : (Z.stalkQuotientEquiv z) ((Ideal.Quotient.mk (Z.stalkIdeal (Z.subschemeι z))) a) = (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap Z.subschemeι z)) a

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.residueFieldStalkEquiv {X : Scheme} (Z : X.IdealSheafData) (z : ↥Z.subscheme) : IsLocalRing.ResidueField ↑(X.presheaf.stalk (Z.subschemeι z)) ≃+* IsLocalRing.ResidueField ↑(Z.subscheme.presheaf.stalk z)

The residue fields of 𝒪_{X,ι z} and 𝒪_{V(Z),z} agree (the stalk map is a surjective local homomorphism).

Equations

• Z.residueFieldStalkEquiv z = RingEquiv.ofBijective (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.subschemeι z))) ⋯

theorem AlgebraicGeometry.Scheme.IdealSheafData.residueFieldStalkEquiv_residue {X : Scheme} (Z : X.IdealSheafData) (z : ↥Z.subscheme) (r : ↑(X.presheaf.stalk (Z.subschemeι z))) : (Z.residueFieldStalkEquiv z) ((IsLocalRing.residue ↑(X.presheaf.stalk (Z.subschemeι z))) r) = (IsLocalRing.residue ↑(Z.subscheme.presheaf.stalk z)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap Z.subschemeι z)) r)

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_singleton_of_subschemeι_eq {X : Scheme} (Z : X.IdealSheafData) {z : ↥Z.subscheme} {x : ↥X} (hzx : Z.subschemeι z = x) (hx : IsClosed {x}) : IsClosed {z}

A closed point of X in the support of Z is a closed point of V(Z).