Documentation

TauCeti.AlgebraicGeometry.Scheme.ZeroLocusComponents

Irreducible components of the zero locus of a global function #

Let X be an integral locally Noetherian scheme and a a nonzero global function on X. This file identifies the irreducible components of the closed subset V(a) where a vanishes: their generic points, which are the points of V(a) maximal for the specialization order among the points of V(a), are exactly the codimension-one points of X lying in V(a). This is Krull's principal ideal theorem read on the scheme: at a generic point x of a component of V(a), the maximal ideal of the local ring 𝒪_{X, x} is a minimal prime over the germ of a, so it has height at most one, and it has height at least one because a is a unit at the generic point of X, which therefore does not lie in V(a).

The points of the spectrum of the local ring 𝒪_{X, x} are the generizations of x, and the germ of a lies in the prime corresponding to a generization y exactly when a vanishes at y; this is TauCeti.AlgebraicGeometry.Scheme.fromSpecStalk_mem_basicOpen_iff, which is what turns maximality of x in V(a) into minimality of the maximal ideal over the germ of a.

Conversely a codimension-one point of V(a) is maximal there, since its only proper generization is the generic point of X. Every point of V(a) specializes from such a maximal point, because coheights in a locally Noetherian scheme are finite and a generization inside V(a) of least coheight is maximal.

The application is to the special fibre of a scheme over a discrete valuation ring: the special fibre is the zero locus of a uniformizer, so its irreducible components are the codimension-one points of the total space at which the uniformizer vanishes.

Main results #

References #

source
theorem TauCeti.AlgebraicGeometry.Scheme.fromSpecStalk_mem_basicOpen_iff {X : AlgebraicGeometry.Scheme} {U : X.Opens} {x : ↥X} (hxU : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) (q : ↥(AlgebraicGeometry.Spec (X.presheaf.stalk x))) :
(X.fromSpecStalk x) q ∈ X.basicOpen f ↔ (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hxU)) f ∉ q.asIdeal

A point of the spectrum of the local ring of X at x, that is, a generization of x, lies in the basic open of a section f exactly when the germ of f at x lies outside the corresponding prime ideal.

source
theorem TauCeti.AlgebraicGeometry.Scheme.germ_mem_maximalIdeal_of_mem_zeroLocus {X : AlgebraicGeometry.Scheme} {a : ↑(X.presheaf.obj (Opposite.op ⊤))} {x : ↥X} (hx : x ∈ X.zeroLocus {a}) :
(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) a ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)

The germ of a global function at a point of its zero locus lies in the maximal ideal of the local ring there.

source
theorem TauCeti.AlgebraicGeometry.Scheme.maximalIdeal_mem_minimalPrimes_of_maximal {X : AlgebraicGeometry.Scheme} {a : ↑(X.presheaf.obj (Opposite.op ⊤))} {x : ↥X} (hx : Maximal (fun (x : ↥X) => x ∈ X.zeroLocus {a}) x) :
IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∈ (Ideal.span {(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) a}).minimalPrimes

At a maximal point x of the zero locus of a global function a, the maximal ideal of the local ring is a minimal prime over the germ of a: a smaller prime containing the germ would be a generization of x inside the zero locus.

source
theorem TauCeti.AlgebraicGeometry.Scheme.genericPoint_mem_basicOpen {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : a ≠ 0) :
genericPoint ↥X ∈ X.basicOpen a

A nonzero global function on an integral scheme is a unit at the generic point.

source
theorem TauCeti.AlgebraicGeometry.Scheme.genericPoint_notMem_zeroLocus {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : a ≠ 0) :
genericPoint ↥X ∉ X.zeroLocus {a}

A nonzero global function on an integral scheme does not vanish at the generic point.

source
theorem TauCeti.AlgebraicGeometry.Scheme.coheight_lt_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) :
Order.coheight x < ⊤

On a locally Noetherian scheme every point has finite coheight: the coheight is the Krull dimension of the Noetherian local ring at the point.

source
theorem TauCeti.AlgebraicGeometry.Scheme.exists_maximal_mem_zeroLocus_specializes {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} {x : ↥X} (hx : x ∈ X.zeroLocus {a}) :
∃ (y : ↥X), Maximal (fun (x : ↥X) => x ∈ X.zeroLocus {a}) y ∧ y ⤳ x

Every point of the zero locus of a global function on a locally Noetherian scheme lies on an irreducible component of that zero locus: it specializes from a maximal point of the zero locus.

source
theorem TauCeti.AlgebraicGeometry.Scheme.coheight_eq_one_of_maximal_mem_zeroLocus {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsIntegral X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : a ≠ 0) {x : ↥X} (hx : Maximal (fun (x : ↥X) => x ∈ X.zeroLocus {a}) x) :
Order.coheight x = 1

Krull's principal ideal theorem on a scheme. A maximal point of the zero locus of a nonzero global function on an integral locally Noetherian scheme, that is, the generic point of an irreducible component of that zero locus, has coheight one.

source
theorem TauCeti.AlgebraicGeometry.Scheme.maximal_mem_zeroLocus_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsIntegral X] {a : ↑(X.presheaf.obj (Opposite.op ⊤))} (ha : a ≠ 0) {x : ↥X} :
Maximal (fun (x : ↥X) => x ∈ X.zeroLocus {a}) x ↔ x ∈ X.zeroLocus {a} ∧ Order.coheight x = 1

The maximal points of the zero locus of a nonzero global function on an integral locally Noetherian scheme are exactly the codimension-one points of the scheme lying in it.