Irreducible components and multiplicities of the special fibre

Let R be a local ring of Krull dimension at most one (Ring.DimensionLEOne R), for instance a discrete valuation ring, and let X → Spec R be a scheme over R. The special fibre of X is the fibre over the closed point of Spec R. For a nonzero element π of the maximal ideal of R, for instance a uniformizer, the special fibre is the zero locus of the pullback of π to X: a point of X lies over the closed point exactly when π vanishes there, because the only prime of R containing π is the maximal ideal.

When X is integral and locally Noetherian and its generic point lies over the generic point of Spec R, as it does when X → Spec R is flat, the results of TauCeti.AlgebraicGeometry.Scheme.ZeroLocusComponents describe the special fibre: its irreducible components are the closures of the codimension-one points of X lying over the closed point, every point of the special fibre lies on such a component, and, for X Noetherian, there are finitely many components. The divisor of the pullback of π is an effective Weil divisor on X supported exactly on these components, so that

div_X(π) = ∑ᵢ mᵢ [Cᵢ], with mᵢ = ord_{Cᵢ}(π) > 0

the coefficient of the component Cᵢ in the divisor of π. When R is a discrete valuation ring and π is a uniformizer, this divisor is the special fibre X_s and mᵢ is the multiplicity of Cᵢ in X_s; these multiplicities and the finite component set are the first invariants of the numerical type of a regular model of a curve over a discrete valuation ring. For a general nonzero π in the maximal ideal the coefficients depend on π: replacing π by π ^ 2 doubles them.

The statements are phrased for an explicit structure morphism toBase : X ⟶ Spec R rather than for a bundled model, so that they apply to the total space M.total of any TauCeti.Model through M.toBase, whose flatness is an instance. For a discrete valuation ring the hypothesis maximalIdeal R ≠ ⊥ is IsDiscreteValuationRing.not_a_field R, and the dimension hypothesis is the instance Ring.DimensionLEOne.principal_ideal_ring. The results about toBase are stated in the namespace AlgebraicGeometry.Scheme.Hom, so they are available by dot notation on the structure morphism.

Main results

• TauCeti.range_specialFiberι: the special fibre of a scheme over a local ring is the preimage of the closed point;
• PrimeSpectrum.mem_asIdeal_iff_eq_closedPoint: in a local ring of dimension at most one, a nonzero element of the maximal ideal lies in a prime exactly when that prime is the maximal ideal;
• AlgebraicGeometry.Scheme.Hom.base_eq_closedPoint_iff_mem_zeroLocus and AlgebraicGeometry.Scheme.Hom.preimage_closedPoint_eq_zeroLocus: the special fibre is the zero locus of the pullback of a nonzero element of the maximal ideal;
• AlgebraicGeometry.Scheme.Hom.base_genericPoint_ne_closedPoint: the generic point of an irreducible scheme flat over R does not lie in the special fibre;
• AlgebraicGeometry.Scheme.Hom.maximal_base_eq_closedPoint_iff: the generic points of the irreducible components of the special fibre are the codimension-one points of X lying in it;
• AlgebraicGeometry.Scheme.Hom.exists_maximal_base_eq_closedPoint_specializes: every point of the special fibre lies on an irreducible component of it;
• AlgebraicGeometry.Scheme.Hom.finite_setOf_base_eq_closedPoint: the special fibre of a Noetherian integral scheme has finitely many irreducible components;
• AlgebraicGeometry.Scheme.Hom.ord_germToFunctionField_appTop_pos_iff: the order of the pullback of π at a codimension-one point is positive exactly when the point lies in the special fibre;
• AlgebraicGeometry.Scheme.Hom.mem_support_principalDivisor_appTop: the divisor of the pullback of π is supported exactly on the components of the special fibre.

References

• The Stacks Project, Section 55.9, the geometry of a regular model, in particular the description of the special fibre as the divisor of a uniformizer.
• Q. Liu, Algebraic Geometry and Arithmetic Curves, Section 8.3, on models of curves and the multiplicities of the components of their special fibres.

theorem TauCeti.range_specialFiberι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) : Set.range ⇑(specialFiberι R toBase) = ⇑toBase ⁻¹' {IsLocalRing.closedPoint R}

The special fibre of a scheme over a local ring is, as a set, the preimage of the closed point: the special fibre is isomorphic over X to Mathlib's fibre of toBase at the closed point.

theorem PrimeSpectrum.mem_asIdeal_iff_eq_closedPoint {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] (p : PrimeSpectrum R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) : π ∈ p.asIdeal ↔ p = IsLocalRing.closedPoint R

In a local ring of Krull dimension at most one, a nonzero element of the maximal ideal lies in a prime ideal exactly when that prime is the maximal ideal.

theorem AlgebraicGeometry.Scheme.Hom.base_eq_closedPoint_iff_mem_zeroLocus {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) (x : ↥X) : toBase x = IsLocalRing.closedPoint R ↔ x ∈ X.zeroLocus {(CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π)}

A point of a scheme over a local ring of dimension at most one lies over the closed point exactly when the pullback of a nonzero element π of the maximal ideal vanishes at it.

theorem AlgebraicGeometry.Scheme.Hom.preimage_closedPoint_eq_zeroLocus {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) : ⇑toBase ⁻¹' {IsLocalRing.closedPoint R} = X.zeroLocus {(CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π)}

The special fibre of a scheme over a local ring of dimension at most one is the zero locus of the pullback of a nonzero element of the maximal ideal.

theorem AlgebraicGeometry.Scheme.Hom.base_genericPoint_ne_closedPoint {R : Type u} [CommRing R] [IsLocalRing R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IrreducibleSpace ↥X] [IsDomain R] [Flat toBase] (hR : IsLocalRing.maximalIdeal R ≠ ⊥) : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R

The generic point of an irreducible scheme flat over a local domain which is not a field does not lie in the special fibre.

theorem AlgebraicGeometry.Scheme.Hom.appTop_ΓSpecIso_inv_ne_zero {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IrreducibleSpace ↥X] (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) : (CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π) ≠ 0

If the generic point of an irreducible scheme over a one-dimensional local ring does not lie in the special fibre, the pullback of a nonzero element of the maximal ideal is a nonzero global function.

theorem AlgebraicGeometry.Scheme.Hom.germToFunctionField_appTop_ne_zero {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsIntegral X] (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) : (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) ((CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π)) ≠ 0

The pullback of a nonzero element of the maximal ideal is a nonzero rational function.

theorem AlgebraicGeometry.Scheme.Hom.maximal_base_eq_closedPoint_iff {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsIntegral X] [IsLocallyNoetherian X] (hR : IsLocalRing.maximalIdeal R ≠ ⊥) (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) {x : ↥X} : Maximal (fun (y : ↥X) => toBase y = IsLocalRing.closedPoint R) x ↔ toBase x = IsLocalRing.closedPoint R ∧ Order.coheight x = 1

The irreducible components of the special fibre. For an integral locally Noetherian scheme over a local ring of dimension at most one which is not a field, whose generic point does not lie in the special fibre, the generic points of the irreducible components of the special fibre, that is, its points maximal for the specialization order, are exactly the codimension-one points of X lying in the special fibre.

theorem AlgebraicGeometry.Scheme.Hom.exists_maximal_base_eq_closedPoint_specializes {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsLocallyNoetherian X] (hR : IsLocalRing.maximalIdeal R ≠ ⊥) {x : ↥X} (hx : toBase x = IsLocalRing.closedPoint R) : ∃ (y : ↥X), Maximal (fun (y : ↥X) => toBase y = IsLocalRing.closedPoint R) y ∧ y ⤳ x

Every point of the special fibre of a locally Noetherian scheme over a local ring of dimension at most one which is not a field lies on an irreducible component of the special fibre.

theorem AlgebraicGeometry.Scheme.Hom.ord_germToFunctionField_appTop_pos_iff {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsIntegral X] [IsLocallyNoetherian X] (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) {x : ↥X} (hx : Order.coheight x = 1) : 0 < ord ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) ((CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π))) x ↔ toBase x = IsLocalRing.closedPoint R

At a codimension-one point of X, the order of vanishing of the pullback of a nonzero element π of the maximal ideal is positive exactly when the point lies in the special fibre. This order is the coefficient of the corresponding component of the special fibre in the divisor of the pullback of π; when R is a discrete valuation ring and π is a uniformizer, it is the multiplicity of that component in the special fibre.

theorem AlgebraicGeometry.Scheme.Hom.finite_setOf_base_eq_closedPoint {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsIntegral X] [IsNoetherian X] (hR : IsLocalRing.maximalIdeal R ≠ ⊥) (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) : {x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X | toBase ↑x = IsLocalRing.closedPoint R}.Finite

The special fibre of a Noetherian integral scheme over a local ring of dimension at most one which is not a field, whose generic point does not lie in the special fibre, has finitely many irreducible components: only finitely many codimension-one points of X lie in it.

theorem AlgebraicGeometry.Scheme.Hom.mem_support_principalDivisor_appTop {R : Type u} [CommRing R] [IsLocalRing R] [Ring.DimensionLEOne R] {X : Scheme} (toBase : X ⟶ Spec ↧R) [IsIntegral X] [IsNoetherian X] (hη : toBase (genericPoint ↥X) ≠ IsLocalRing.closedPoint R) {π : R} (hπ : π ∈ IsLocalRing.maximalIdeal R) (hπ0 : π ≠ 0) (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X) : x ∈ ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofScheme X).principalDivisor (Additive.ofMul (Units.mk0 ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) ((CategoryTheory.ConcreteCategory.hom (appTop toBase)) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) π))) ⋯))).support ↔ toBase ↑x = IsLocalRing.closedPoint R

The divisor of a uniformizer is supported on the special fibre. The principal divisor of the pullback of a nonzero element π of the maximal ideal is supported exactly on the codimension-one points of the special fibre, the generic points of its irreducible components. Together with TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_principalDivisor_ofMul_mk0 this is the decomposition div_X(π) = ∑ᵢ mᵢ [Cᵢ] with positive coefficients mᵢ; when R is a discrete valuation ring and π is a uniformizer, these are the multiplicities of the components of the special fibre.