Coordinate-free Riemann–Roch

This file exposes the Riemann–Roch stack over divisors indexed by intrinsic valuation-subring places. The kernel-checked chart proofs are transported across chartToPlace.

Main definitions and results

• FunctionField.RRspace, FunctionField.ell, and FunctionField.genus.
• FunctionField.AdeleSpace and FunctionField.adeleFilt.
• FunctionField.IsCanonical and FunctionField.duality.
• FunctionField.riemann_roch and coordinate-free corollaries C1–C6.

def FunctionField.memRRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) (f : K) : Prop

A function belongs to the intrinsic Riemann–Roch space of D when its normalized valuation at every place is bounded by the coefficient of D there.

Equations

• FunctionField.memRRspace k K D f = ∀ (v : FunctionField.Place k K), v.valuation f ≤ WithZero.exp (D v)

theorem FunctionField.memRRspace.zero_mem {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (D : Divisor k K) : memRRspace k K D 0

theorem FunctionField.memRRspace.add_mem {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {D : Divisor k K} {f g : K} (hf : memRRspace k K D f) (hg : memRRspace k K D g) : memRRspace k K D (f + g)

theorem FunctionField.memRRspace.smul_mem {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {D : Divisor k K} (c : k) {f : K} (hf : memRRspace k K D f) : memRRspace k K D (c • f)

def FunctionField.RRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : Submodule k K

The Riemann–Roch space of an intrinsic divisor.

Equations

• FunctionField.RRspace k K D = { carrier := {f : K | FunctionField.memRRspace k K D f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def FunctionField.ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : ℕ

The Riemann–Roch dimension of an intrinsic divisor.

Equations

• FunctionField.ell k K D = Module.finrank k ↥(FunctionField.RRspace k K D)

noncomputable def FunctionField.defect (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : ℤ

The defect of an intrinsic divisor.

Equations

• FunctionField.defect k K D = FunctionField.Divisor.deg k K D + 1 - ↑(FunctionField.ell k K D)

noncomputable def FunctionField.genus (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : ℕ

The intrinsic genus is the supremum of the defects of all intrinsic divisors. The Riemann–Roch argument below proves that this supremum is attained and agrees with every chart calculation.

Equations

• FunctionField.genus k K = (sSup {d : ℤ | ∃ (D : FunctionField.Divisor k K), FunctionField.defect k K D = d}).toNat

theorem FunctionField.memRRspace_equivChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) (f : K) : memRRspace k K D f ↔ Chart.memRRspace k K ((divisorEquivChart k K).symm D) f

The intrinsic membership condition agrees with the coordinate construction.

theorem FunctionField.RRspace_eq_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : RRspace k K D = Chart.RRspace k K ((divisorEquivChart k K).symm D)

The intrinsic Riemann–Roch space is the chart space after reindexing divisors.

theorem FunctionField.ell_eq_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : ell k K D = Chart.ell k K ((divisorEquivChart k K).symm D)

Riemann–Roch dimension is preserved by the chart equivalence.

noncomputable def FunctionField.indexOfSpecialty (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (D : Divisor k K) : ℕ

The index of specialty of an intrinsic divisor.

Equations

• FunctionField.indexOfSpecialty k K D = (↑(FunctionField.ell k K D) - (FunctionField.Divisor.deg k K D + 1 - ↑(FunctionField.genus k K))).toNat

noncomputable def FunctionField.finrankAdeleQuotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : ℕ

The dimension of the intrinsic adele quotient by A(D) plus the diagonal.

Equations

• FunctionField.finrankAdeleQuotient k K D = Module.finrank k (↥(FunctionField.AdeleSpace k K) ⧸ FunctionField.adeleFilt k K D + FunctionField.diagonalSubmodule k K)

@[simp]

theorem FunctionField.Divisor.chart_deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : Chart.deg k K ((divisorEquivChart k K).symm D) = deg k K D

Pulling an intrinsic divisor back to the chart preserves degree.

theorem FunctionField.defect_eq_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : defect k K D = Chart.defect k K ((divisorEquivChart k K).symm D)

Intrinsic defect is preserved by the chart equivalence.

theorem FunctionField.genus_eq_genusChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : genus k K = Chart.genus k K

The intrinsic supremum definition of genus agrees with the chart construction.

theorem FunctionField.chart_isCanonical_iff_degree_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (E : Chart.DivisorA k K) : Chart.IsCanonical k K E ↔ Chart.deg k K E = 2 * ↑(Chart.genus k K) - 2 ∧ Chart.ell k K E = Chart.genus k K

The numerical characterization of a canonical coordinate divisor.

theorem FunctionField.isCanonical_iff_deg_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (W : Divisor k K) : IsCanonical k K W ↔ Divisor.deg k K W = 2 * ↑(genus k K) - 2 ∧ ell k K W = genus k K

A divisor is canonical exactly when it has degree 2g - 2 and Riemann–Roch dimension g.

theorem FunctionField.indexOfSpecialty_eq_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : Divisor k K) : indexOfSpecialty k K D = Chart.indexOfSpecialty k K ((divisorEquivChart k K).symm D)

The intrinsic specialty index agrees with the coordinate construction.

noncomputable def FunctionField.adeleQuotientEquivChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : (↥(AdeleSpace k K) ⧸ adeleFilt k K D + diagonalSubmodule k K) ≃ₗ[k] ↥(Chart.AdeleSpace k K) ⧸ Chart.adeleFilt k K ((divisorEquivChart k K).symm D) + Chart.diagonalSubmodule k K

The intrinsic adele quotient is linearly equivalent to its chart presentation.

Equations

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

theorem FunctionField.finrankAdeleQuotient_eq_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : Divisor k K) : finrankAdeleQuotient k K D = Chart.finrankAdeleQuotient k K ((divisorEquivChart k K).symm D)

The intrinsic and chart adele quotients have the same dimension.

theorem FunctionField.finrank_adele_quotient (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : Divisor k K) : finrankAdeleQuotient k K D = indexOfSpecialty k K D

The intrinsic adele quotient dimension is the index of specialty.

noncomputable def FunctionField.sandwichRank (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : Divisor k K) : ℤ

The rank change in the intrinsic filtration-and-diagonal sandwich.

Equations

• FunctionField.sandwichRank k K D E = FunctionField.Chart.sandwichRank k K ((FunctionField.divisorEquivChart k K).symm D) ((FunctionField.divisorEquivChart k K).symm E)

theorem FunctionField.sandwich (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D E : Divisor k K} (h : D ≤ E) : sandwichRank k K D E = Divisor.deg k K E - ↑(ell k K E) - (Divisor.deg k K D - ↑(ell k K D))

The intrinsic sandwich rank is the change in deg D - ell(D).

theorem FunctionField.WeilDifferential.finrank_differentialSpace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : Divisor k K) : Module.finrank k ↥(differentialSpace D) = indexOfSpecialty k K D

The dimension of intrinsic Omega(D) is the index of specialty of D.

theorem FunctionField.exists_isCanonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (W : Divisor k K), IsCanonical k K W

Every function field admits an intrinsic canonical divisor.

theorem FunctionField.duality (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) : ell k K (W - D) = indexOfSpecialty k K D

Coordinate-free duality.

theorem FunctionField.riemann_ineq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : Divisor k K) : ↑(ell k K D) ≥ Divisor.deg k K D + 1 - ↑(genus k K)

Riemann's inequality for intrinsic divisors.

theorem FunctionField.riemann_roch (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) : ↑(ell k K D) = Divisor.deg k K D + 1 - ↑(genus k K) + ↑(ell k K (W - D))

The coordinate-free Riemann–Roch theorem.

theorem FunctionField.ell_canonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) : ell k K W = genus k K

C1: a canonical divisor has Riemann–Roch dimension equal to the genus.

theorem FunctionField.deg_canonical (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) : Divisor.deg k K W = 2 * ↑(genus k K) - 2

C2: a canonical divisor has degree 2g - 2.

theorem FunctionField.ell_eq_of_deg_ge (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) (hdeg : Divisor.deg k K D ≥ 2 * ↑(genus k K) - 1) : ↑(ell k K D) = Divisor.deg k K D + 1 - ↑(genus k K)

C3: divisors of degree at least 2g - 1 are nonspecial.

theorem FunctionField.indexOfSpecialty_eq_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) : ↑(indexOfSpecialty k K D) = ↑(ell k K (W - D))

C4: the specialty index is ℓ(W-D).

theorem FunctionField.clifford_of_ell_pos (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) (hℓD : 0 < ell k K D) (hℓW : 0 < ell k K (W - D)) : 2 * (↑(ell k K D) - 1) ≤ Divisor.deg k K D

The core Clifford inequality for intrinsic divisors: whenever ℓ(D) and ℓ(W − D) are both positive for a canonical W, 2(ℓ(D) − 1) ≤ deg D. No degree bounds are needed.

theorem FunctionField.clifford (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : Divisor k K} (hW : IsCanonical k K W) (D : Divisor k K) (_hdeg₀ : 0 ≤ Divisor.deg k K D) (_hdeg₁ : Divisor.deg k K D ≤ 2 * ↑(genus k K) - 2) (hℓD : 0 < ell k K D) (hℓW : 0 < ell k K (W - D)) : 2 * (↑(ell k K D) - 1) ≤ Divisor.deg k K D

C5: Clifford's inequality for intrinsic divisors in its textbook form. The degree bounds 0 ≤ deg D ≤ 2g − 2 are kept for fidelity to the standard statement but are not needed; see clifford_of_ell_pos.

theorem FunctionField.exists_nonspecial_divisor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ∃ (D : Divisor k K), indexOfSpecialty k K D = 0

C6: there exists an intrinsic nonspecial divisor.