The special fibre as the zero scheme of the maximal ideal

Let X → Spec R be a scheme over a local ring R with maximal ideal 𝔪. Its special fibre is the base change X ×_{Spec R} Spec (R ⧸ 𝔪), a closed subscheme of X. This file identifies that closed subscheme: its ideal sheaf is the quasi-coherent ideal sheaf 𝔪·𝒪_X generated by the pullbacks of the elements of 𝔪. When 𝔪 = (π) is principal, for instance when R is a discrete valuation ring and π a uniformizer, the special fibre is therefore the zero scheme V(π) of the single global function π pulled back to X.

The identification X_s = V(π) holds for every scheme over R: this file places no hypothesis on X. Whether V(π) is an effective Cartier divisor is a separate question, which depends on X: it is one exactly when the pullback of π is a non-zero-divisor locally on X, as it is when π is a non-zero-divisor of R (for instance a uniformizer of a discrete valuation ring) and X is flat over R, and it fails for instance for X = Spec (R ⧸ 𝔪), where π pulls back to zero and X_s = X. For a discrete valuation ring and an integral, locally Noetherian X flat over R, this file and TauCeti.AlgebraicGeometry.SpecialFiber.Components give the two halves of X_s = div_X(π): the Weil divisor of π is supported on the components of X_s with their multiplicities, and the closed subscheme cut out by the equation π is X_s itself. Identifying V(π) with the divisor of π through the CartierDivisor API is not done here.

Main results

• TauCeti.ker_specialFiberι: the ideal sheaf of the special fibre is 𝔪·𝒪_X;
• TauCeti.ker_specialFiberι_eq_ofIdealTop_span: when 𝔪 = (π), it is the ideal sheaf generated by the pullback of π;
• TauCeti.specialFiberIsoSubscheme: the special fibre is isomorphic over X to the zero scheme of 𝔪·𝒪_X, and TauCeti.isPullback_subschemeι_specialFiber records the resulting pullback square.

References

• The Stacks Project, Section 55.9, the special fibre of a regular model as the divisor of a uniformizer.

theorem TauCeti.ker_specialFiberι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : AlgebraicGeometry.Scheme.Hom.ker (specialFiberι R toBase) = AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))

The special fibre is cut out by the maximal ideal. The ideal sheaf of the special fibre of a scheme over a local ring is the ideal sheaf 𝔪·𝒪_X generated by the pullbacks of the elements of the maximal ideal 𝔪 of the base.

theorem TauCeti.ker_specialFiberι_eq_ofIdealTop_span {R : Type u} [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {π : R} (hπ : IsLocalRing.maximalIdeal R = Ideal.span {π}) : AlgebraicGeometry.Scheme.Hom.ker (specialFiberι R toBase) = AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.span {(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv) π)})

The special fibre is the zero scheme of a uniformizer. If the maximal ideal of the base is generated by π, the ideal sheaf of the special fibre is generated by the pullback of π: the special fibre is the zero scheme V(π) of the pullback of π to the total space.

noncomputable def TauCeti.specialFiberIsoSubscheme (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : (specialFiber R toBase).left ≅ (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subscheme

The special fibre of a scheme over a local ring is isomorphic, as a closed subscheme of the total space, to the zero scheme of the ideal sheaf 𝔪·𝒪_X generated by the maximal ideal of the base.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.specialFiberIsoSubscheme_hom_subschemeι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoSubscheme R toBase).hom (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subschemeι = specialFiberι R toBase

The identification of the special fibre with the zero scheme of 𝔪·𝒪_X is compatible with the inclusions into the total space.

@[simp]

theorem TauCeti.specialFiberIsoSubscheme_hom_subschemeι_assoc (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoSubscheme R toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subschemeι h) = CategoryTheory.CategoryStruct.comp (specialFiberι R toBase) h

The identification of the special fibre with the zero scheme of 𝔪·𝒪_X is compatible with the inclusions into the total space.

@[simp]

theorem TauCeti.specialFiberIsoSubscheme_inv_specialFiberι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoSubscheme R toBase).inv (specialFiberι R toBase) = (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subschemeι

The inverse identification of the zero scheme of 𝔪·𝒪_X with the special fibre is compatible with the inclusions into the total space.

@[simp]

theorem TauCeti.specialFiberIsoSubscheme_inv_specialFiberι_assoc (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoSubscheme R toBase).inv (CategoryTheory.CategoryStruct.comp (specialFiberι R toBase) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subschemeι h

The inverse identification of the zero scheme of 𝔪·𝒪_X with the special fibre is compatible with the inclusions into the total space.

theorem TauCeti.isPullback_subschemeι_specialFiber (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : CategoryTheory.IsPullback (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop (Ideal.map ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop toBase)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) (IsLocalRing.maximalIdeal R))).subschemeι (CategoryTheory.CategoryStruct.comp (specialFiberIsoSubscheme R toBase).inv (specialFiber R toBase).hom) toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))))

The zero scheme of 𝔪·𝒪_X, with its inclusion into the total space and its induced morphism to the spectrum of the residue field, is a pullback of X → Spec R and Spec (R ⧸ 𝔪) → Spec R: it is the special fibre.