Codimension-one points of a scheme

A point of a scheme has codimension one when its coheight for the specialization order is one, equivalently when it is the generic point of an irreducible closed subset of codimension one. This file introduces the subtype of such points and records the one order-theoretic fact about them that does not mention any further structure: a codimension-one point has no codimension-one generization other than itself.

The type is used both by the divisor layer, where a codimension-one point represents a prime divisor, and by the place layer, where it is the centre of a function-field place; it is defined here so that neither layer has to depend on the other.

Main declarations

• TauCeti.AlgebraicGeometry.CodimensionOnePoint: the codimension-one points of a scheme.
• TauCeti.AlgebraicGeometry.CodimensionOnePoint.eq_of_specializes: a codimension-one generization of a codimension-one point is equal to it.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.CodimensionOnePoint (X : AlgebraicGeometry.Scheme) : Type u

A codimension-one point of a scheme. Such a point is the generic point of a prime divisor.

Equations

• TauCeti.AlgebraicGeometry.CodimensionOnePoint X = { x : ↥X // Order.coheight x = 1 }

theorem TauCeti.AlgebraicGeometry.CodimensionOnePoint.eq_of_specializes {X : AlgebraicGeometry.Scheme} {x y : CodimensionOnePoint X} (h : ↑y ⤳ ↑x) : y = x

A codimension-one point admits no codimension-one generization other than itself: a strict generization has strictly smaller coheight, and both points have coheight one.