Weil divisors on schemes

This file specializes the combinatorial type WeilDivisor to schemes. A prime divisor is represented by its generic point, which is a point of codimension one, and a scheme-theoretic Weil divisor is a finite formal integer sum of such points.

Mathlib's AlgebraicCycle X ℤ allows locally finite support in every codimension. The map SchemeWeilDivisor.toAlgebraicCycle extends a Weil divisor by zero away from codimension one. Its image is characterized by finiteCodimensionOneCycles, the subgroup of algebraic cycles with finite support entirely in codimension one, and SchemeWeilDivisor.equivFiniteCodimensionOneCycles identifies the two descriptions.

The coefficient, support, effectivity, and point-divisor API is inherited directly from WeilDivisor; no scheme-specific copies of those declarations are introduced.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve: Weil divisors ⊕_x ℤ", by supplying the scheme-theoretic codimension-one specialization needed before principal divisors can be constructed from Scheme.ord.

@[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 }

@[reducible, inline]

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

A Weil divisor on a scheme is a finite formal integer sum of its codimension-one points.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor X = TauCeti.AlgebraicGeometry.WeilDivisor (TauCeti.AlgebraicGeometry.CodimensionOnePoint X)

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toAlgebraicCycle {X : AlgebraicGeometry.Scheme} : SchemeWeilDivisor X →+ AlgebraicGeometry.AlgebraicCycle X ℤ

Extend a scheme-theoretic Weil divisor by zero away from codimension one, obtaining an algebraic cycle on the underlying scheme.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toAlgebraicCycle_apply {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) (x : CodimensionOnePoint X) : (toAlgebraicCycle D) ↑x = D x

Extension by zero preserves the coefficient at a codimension-one point.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toAlgebraicCycle_apply_of_coheight_ne_one {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) (x : ↥X) (hx : Order.coheight x ≠ 1) : (toAlgebraicCycle D) x = 0

Extension by zero vanishes at points whose codimension is not one.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.support_toAlgebraicCycle {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) : Function.locallyFinsuppWithin.support (toAlgebraicCycle D) = Subtype.val '' ↑D.support

The support of a scheme-theoretic Weil divisor viewed as an algebraic cycle is the image of its finite support under the inclusion of codimension-one points.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_support_toAlgebraicCycle {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) : (Function.locallyFinsuppWithin.support (toAlgebraicCycle D)).Finite

A scheme-theoretic Weil divisor has finite support when regarded as an algebraic cycle.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coheight_eq_one_of_mem_support_toAlgebraicCycle {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) {x : ↥X} (hx : x ∈ Function.locallyFinsuppWithin.support (toAlgebraicCycle D)) : Order.coheight x = 1

The cycle associated to a scheme-theoretic Weil divisor is supported in codimension one.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toAlgebraicCycle_injective {X : AlgebraicGeometry.Scheme} : Function.Injective ⇑toAlgebraicCycle

Extension by zero embeds scheme-theoretic Weil divisors into algebraic cycles.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toAlgebraicCycle_inj {X : AlgebraicGeometry.Scheme} {D E : SchemeWeilDivisor X} : toAlgebraicCycle D = toAlgebraicCycle E ↔ D = E

Two scheme-theoretic Weil divisors have the same associated cycle exactly when they are equal.

def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finiteCodimensionOneCycles (X : AlgebraicGeometry.Scheme) : AddSubgroup (AlgebraicGeometry.AlgebraicCycle X ℤ)

Algebraic cycles with finite support contained in codimension one.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.mem_finiteCodimensionOneCycles_iff {X : AlgebraicGeometry.Scheme} {C : AlgebraicGeometry.AlgebraicCycle X ℤ} : C ∈ finiteCodimensionOneCycles X ↔ (Function.locallyFinsuppWithin.support C).Finite ∧ ∀ x ∈ Function.locallyFinsuppWithin.support C, Order.coheight x = 1

Membership in finiteCodimensionOneCycles means finite support contained in codimension one.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFiniteCodimensionOneCycles {X : AlgebraicGeometry.Scheme} : SchemeWeilDivisor X ≃+ ↥(finiteCodimensionOneCycles X)

Scheme-theoretic Weil divisors are additively equivalent to the finite algebraic cycles supported entirely in codimension one.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.coe_equivFiniteCodimensionOneCycles_apply {X : AlgebraicGeometry.Scheme} (D : SchemeWeilDivisor X) : ↑(equivFiniteCodimensionOneCycles D) = toAlgebraicCycle D

The forward direction of equivFiniteCodimensionOneCycles is extension by zero.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.equivFiniteCodimensionOneCycles_symm_apply_apply {X : AlgebraicGeometry.Scheme} (C : ↥(finiteCodimensionOneCycles X)) (x : CodimensionOnePoint X) : (equivFiniteCodimensionOneCycles.symm C) x = ↑C ↑x

The inverse of equivFiniteCodimensionOneCycles recovers coefficients by restriction to codimension-one points.