Cartier divisors on an integral scheme

This file defines Cartier divisors without inventing a meromorphic-function sheaf that Mathlib does not yet have. For an integral scheme X, the function field K(X) is upstream. At a point x, the local Cartier group is

K(X)ˣ / 𝒪_{X,x}ˣ,

where local units enter K(X)ˣ through the canonical map from the stalk. A Cartier divisor is a section of these stalkwise quotients that is locally represented by one nonzero rational function. This is the usual local-equations definition of a Cartier divisor on an integral scheme, expressed without a sheaf quotient.

The construction provides:

• the abelian group Scheme.CartierDivisor X;
• principal divisors and the explicit quotient CartierDivisor.ClassGroup X;
• codimension-one coefficients through Mathlib's Scheme.ord;
• pullback from explicit function-field data that carries local units to local units.

Deliberate boundaries

Mathlib v4.32.1 does not construct a function-field map for an arbitrary morphism of integral schemes, so this file does not claim an unconditional pullback. CartierPullbackData states the exact missing hypotheses. Likewise, coefficient is not packaged as an AlgebraicCycle: the upstream order-of-vanishing API does not yet prove local finiteness of its support. No cycle infrastructure is duplicated here.

noncomputable def AlgebraicGeometry.Scheme.localUnitHom (X : Scheme) [IsIntegral X] (x : ↥X) : (↑(X.presheaf.stalk x))ˣ →* (↑X.functionField)ˣ

Units in the local ring at x, viewed as units of the function field.

Equations

• X.localUnitHom x = Units.map ↑(algebraMap ↑(X.presheaf.stalk x) ↑X.functionField)

noncomputable def AlgebraicGeometry.Scheme.localUnits (X : Scheme) [IsIntegral X] (x : ↥X) : AddSubgroup (Additive (↑X.functionField)ˣ)

Rational functions that are units in the local ring at x, in additive notation.

Equations

• X.localUnits x = Subgroup.toAddSubgroup (X.localUnitHom x).range

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.LocalCartierClass (X : Scheme) [IsIntegral X] (x : ↥X) : Type u

A germ of a Cartier divisor at x: a rational function modulo local units.

Equations

• X.LocalCartierClass x = (Additive (↑X.functionField)ˣ ⧸ X.localUnits x)

noncomputable def AlgebraicGeometry.Scheme.localCartierClass (X : Scheme) [IsIntegral X] (x : ↥X) : Additive (↑X.functionField)ˣ →+ X.LocalCartierClass x

The local Cartier class of a nonzero rational function.

Equations

• X.localCartierClass x = QuotientAddGroup.mk' (X.localUnits x)

@[simp]

theorem AlgebraicGeometry.Scheme.localCartierClass_zero (X : Scheme) [IsIntegral X] (x : ↥X) : (X.localCartierClass x) 0 = 0

@[simp]

theorem AlgebraicGeometry.Scheme.localCartierClass_add (X : Scheme) [IsIntegral X] (x : ↥X) (f g : Additive (↑X.functionField)ˣ) : (X.localCartierClass x) (f + g) = (X.localCartierClass x) f + (X.localCartierClass x) g

theorem AlgebraicGeometry.Scheme.localCartierClass_eq_iff (X : Scheme) [IsIntegral X] (x : ↥X) (f g : Additive (↑X.functionField)ˣ) : (X.localCartierClass x) f = (X.localCartierClass x) g ↔ f - g ∈ X.localUnits x

Two local equations give the same germ precisely when their quotient is a local unit.

def AlgebraicGeometry.Scheme.IsCartier (X : Scheme) [IsIntegral X] (D : (x : ↥X) → X.LocalCartierClass x) : Prop

A family of local Cartier classes is Cartier when it is locally represented by a single nonzero rational function.

Equations

• X.IsCartier D = ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ ∃ (f : Additive (↑X.functionField)ˣ), ∀ y ∈ U, D y = (X.localCartierClass y) f

theorem AlgebraicGeometry.Scheme.isCartier_zero (X : Scheme) [IsIntegral X] : X.IsCartier 0

theorem AlgebraicGeometry.Scheme.IsCartier.add (X : Scheme) [IsIntegral X] {D E : (x : ↥X) → X.LocalCartierClass x} (hD : X.IsCartier D) (hE : X.IsCartier E) : X.IsCartier (D + E)

theorem AlgebraicGeometry.Scheme.IsCartier.neg (X : Scheme) [IsIntegral X] {D : (x : ↥X) → X.LocalCartierClass x} (hD : X.IsCartier D) : X.IsCartier (-D)

def AlgebraicGeometry.Scheme.cartierDivisor (X : Scheme) [IsIntegral X] : AddSubgroup ((x : ↥X) → X.LocalCartierClass x)

The additive subgroup of locally representable families: Cartier divisors on X.

Equations

• X.cartierDivisor = { carrier := X.IsCartier, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.CartierDivisor (X : Scheme) [IsIntegral X] : AddSubgroup ((x : ↥X) → X.LocalCartierClass x)

Cartier divisors on an integral scheme.

Equations

• X.CartierDivisor = X.cartierDivisor

theorem AlgebraicGeometry.Scheme.CartierDivisor.ext {X : Scheme} [IsIntegral X] {D E : ↥X.CartierDivisor} (h : ∀ (x : ↥X), ↑D x = ↑E x) : D = E

Cartier divisors are equal when all of their local classes are equal.

theorem AlgebraicGeometry.Scheme.CartierDivisor.ext_iff {X : Scheme} [IsIntegral X] {D E : ↥X.CartierDivisor} : D = E ↔ ∀ (x : ↥X), ↑D x = ↑E x

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.zero_apply {X : Scheme} [IsIntegral X] (x : ↥X) : ↑0 x = 0

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.add_apply {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) (x : ↥X) : ↑(D + E) x = ↑D x + ↑E x

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.neg_apply {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (x : ↥X) : ↑(-D) x = -↑D x

theorem AlgebraicGeometry.Scheme.CartierDivisor.exists_localEquation {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (x : ↥X) : ∃ (U : X.Opens), x ∈ U ∧ ∃ (f : Additive (↑X.functionField)ˣ), ∀ y ∈ U, ↑D y = (X.localCartierClass y) f

Every Cartier divisor admits a rational local equation around every point.

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.principal (X : Scheme) [IsIntegral X] : Additive (↑X.functionField)ˣ →+ ↥X.CartierDivisor

Principal Cartier divisors, as an additive homomorphism from the multiplicative function field written additively.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.principal X = { toFun := fun (f : Additive (↑X.functionField)ˣ) => ⟨fun (x : ↥X) => (X.localCartierClass x) f, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.ofRationalFunction (X : Scheme) [IsIntegral X] (f : (↑X.functionField)ˣ) : ↥X.CartierDivisor

The principal divisor attached to a nonzero rational function.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.ofRationalFunction X f = (AlgebraicGeometry.Scheme.CartierDivisor.principal X) (Additive.ofMul f)

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.principalDivisors (X : Scheme) [IsIntegral X] : AddSubgroup ↥X.CartierDivisor

The subgroup of principal Cartier divisors.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.principalDivisors X = (AlgebraicGeometry.Scheme.CartierDivisor.principal X).range

instance AlgebraicGeometry.Scheme.CartierDivisor.principalDivisors_normal (X : Scheme) [IsIntegral X] : (principalDivisors X).Normal

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup (X : Scheme) [IsIntegral X] : Type u

Cartier divisor classes: Cartier divisors modulo principal equivalence.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup X = (↥X.CartierDivisor ⧸ AlgebraicGeometry.Scheme.CartierDivisor.principalDivisors X)

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.toClass (X : Scheme) [IsIntegral X] : ↥X.CartierDivisor →+ ClassGroup X

The quotient map from Cartier divisors to Cartier divisor classes.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.toClass X = QuotientAddGroup.mk' (AlgebraicGeometry.Scheme.CartierDivisor.principalDivisors X)

theorem AlgebraicGeometry.Scheme.CartierDivisor.toClass_eq_iff {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) : (toClass X) D = (toClass X) E ↔ D - E ∈ principalDivisors X

The quotient relation defining Cartier divisor classes.

theorem AlgebraicGeometry.Scheme.CartierDivisor.toClass_eq_iff_exists {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) : (toClass X) D = (toClass X) E ↔ ∃ (f : Additive (↑X.functionField)ˣ), (principal X) f = D - E

Explicit principal-equivalence form of the quotient relation.

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.toClass_principal {X : Scheme} [IsIntegral X] (f : Additive (↑X.functionField)ˣ) : (toClass X) ((principal X) f) = 0

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.ordUnitHom {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (x : ↥X) : Additive (↑X.functionField)ˣ →+ ℤ

Order of vanishing of nonzero rational functions, as an additive homomorphism.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.ordUnitHom x = { toFun := fun (f : Additive (↑X.functionField)ˣ) => AlgebraicGeometry.Scheme.ord (↑(Additive.toMul f)) x, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicGeometry.Scheme.CartierDivisor.ordUnitHom_eq_zero_of_mem_localUnits {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (x : ↥X) (f : Additive (↑X.functionField)ˣ) (hf : f ∈ X.localUnits x) : (ordUnitHom x) f = 0

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.localOrder {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (x : ↥X) : X.LocalCartierClass x →+ ℤ

Order of vanishing descends to a local Cartier class because local units have order zero.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.localOrder x = QuotientAddGroup.lift (X.localUnits x) (AlgebraicGeometry.Scheme.CartierDivisor.ordUnitHom x) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.localOrder_localCartierClass {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (x : ↥X) (f : Additive (↑X.functionField)ˣ) : (localOrder x) ((X.localCartierClass x) f) = ord (↑(Additive.toMul f)) x

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.coefficient {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (x : ↥X) : ℤ

The codimension-one coefficient of a Cartier divisor. At other points this uses the upstream junk value 0 of Scheme.ord.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.coefficient D x = (AlgebraicGeometry.Scheme.CartierDivisor.localOrder x) (↑D x)

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.coefficient_add {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D E : ↥X.CartierDivisor) (x : ↥X) : coefficient (D + E) x = coefficient D x + coefficient E x

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.coefficient_principal {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (f : Additive (↑X.functionField)ˣ) (x : ↥X) : coefficient ((principal X) f) x = ord (↑(Additive.toMul f)) x

theorem AlgebraicGeometry.Scheme.CartierDivisor.coefficient_eq_zero_of_coheight_ne_one {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (x : ↥X) (hx : Order.coheight x ≠ 1) : coefficient D x = 0

structure AlgebraicGeometry.Scheme.CartierPullbackData {X Y : Scheme} [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) : Type u

Data sufficient to pull Cartier divisors back along a scheme morphism.

The field map and the condition that it carries local units to local units are explicit because Mathlib v4.32.1 provides no such map for an arbitrary scheme morphism.

• fieldMap : Additive (↑Y.functionField)ˣ →+ Additive (↑X.functionField)ˣ
• map_localUnits (x : ↥X) : Y.localUnits (f x) ≤ AddSubgroup.comap self.fieldMap (X.localUnits x)

noncomputable def AlgebraicGeometry.Scheme.CartierPullbackData.localMap {X Y : Scheme} [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) (p : CartierPullbackData f) (x : ↥X) : Y.LocalCartierClass (f x) →+ X.LocalCartierClass x

The induced map on local Cartier classes.

Equations

• AlgebraicGeometry.Scheme.CartierPullbackData.localMap f p x = QuotientAddGroup.map (Y.localUnits (f x)) (X.localUnits x) p.fieldMap ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.CartierPullbackData.localMap_localCartierClass {X Y : Scheme} [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) (p : CartierPullbackData f) (x : ↥X) (g : Additive (↑Y.functionField)ˣ) : (localMap f p x) ((Y.localCartierClass (f x)) g) = (X.localCartierClass x) (p.fieldMap g)

noncomputable def AlgebraicGeometry.Scheme.CartierPullbackData.pullback {X Y : Scheme} [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) (p : CartierPullbackData f) : ↥Y.CartierDivisor →+ ↥X.CartierDivisor

Pullback of Cartier divisors from explicit compatible function-field data.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.CartierPullbackData.pullback_principal {X Y : Scheme} [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) (p : CartierPullbackData f) (g : Additive (↑Y.functionField)ˣ) : (pullback f p) ((CartierDivisor.principal Y) g) = (CartierDivisor.principal X) (p.fieldMap g)