Genus, Riemann inequality, and the index of specialty

This file defines the genus of a function field and the specialty index i(D).

Main definitions

• FunctionField.defect: deg D + 1 − ℓ(D).
• FunctionField.genus: the maximal defect.
• FunctionField.indexOfSpecialty: ℓ(D) − (deg D + 1 − g).

Main results

• FunctionField.riemann_ineq
• FunctionField.finrank_adele_quotient
• FunctionField.genus_ratFunc
• FunctionField.deg_polarX_eq_finrank

@[instance_reducible]

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncGenus (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

The classical decidable equality on k(X) used by the coordinate places.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncGenus k = Classical.decEq (RatFunc k)

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.defect (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 : DivisorA k K) : ℤ

The defect deg D + 1 − ℓ(D).

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_polarX_eq_finrank (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] : deg k K (polarDivisor k K (XK k K)) = ↑(Module.finrank (RatFunc k) K)

Stichtenoth 1.4.11 for the chart variable X_K (equality; ≤ half proved in Polar.lean).

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_mono' (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 D' : DivisorA k K} (h : D ≤ D') : defect k K D ≤ defect k K D'

Monotonicity of the defect along divisor domination.

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_add_principal (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 : DivisorA k K) (x : Kˣ) : defect k K (D + (principalDivisorA k K) (Additive.ofMul x)) = defect k K D

Defect is unchanged by adding a principal divisor.

theorem MarkoffRiemannRoch.FunctionField.Chart.le_add_principal_of_memRRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D₀ D₁ : DivisorA k K} {f : K} (hf : f ≠ 0) (hmem : memRRspace k K (D₁ - D₀) f) : D₀ ≤ D₁ + (principalDivisorA k K) (Additive.ofMul (Units.mk0 f hf))

From membership in L(D₁ - D₀), the pole divisor of f moves D₀ below D₁ + (f).

theorem MarkoffRiemannRoch.FunctionField.Chart.ell_sub_effective_sub_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] {D E : DivisorA k K} (hE : IsEffective k K E) : ↑(ell k K (D + E)) - deg k K E ≤ ↑(ell k K D)

ℓ(D + E) − deg E ≤ ℓ(D) for effective E.

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_le_of_family (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] (B C : DivisorA k K) (c₀ : ℤ) (hmono : ∀ (r : ℕ), defect k K (C + r • B) ≤ c₀) (hgrow : ∀ (m : ℤ), ∃ (r : ℕ), m ≤ ↑(ell k K (C + r • B))) (D : DivisorA k K) : defect k K D ≤ c₀

Every defect is bounded by c₀ once the pole family has defect ≤ c₀ and grows in rank.

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_le_chart_family (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 : DivisorA k K) : defect k K D ≤ deg k K (basisPoleBound k K ⇑(Module.finBasis (RatFunc k) K)) + 1 - ↑(Module.finrank (RatFunc k) K)

Along the chart pole family, every defect is at most deg C + 1 − n.

theorem MarkoffRiemannRoch.FunctionField.Chart.exists_max_defect (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] : ∃ (g : ℕ), (∀ (D : DivisorA k K), defect k K D ≤ ↑g) ∧ ∃ (D : DivisorA k K), defect k K D = ↑g

Riemann's bounded-defect theorem: the integer defects have a nonnegative maximum.

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.genus (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] : ℕ

The genus of the function field K/k.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.genus k K = Classical.choose ⋯

theorem MarkoffRiemannRoch.FunctionField.Chart.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 : DivisorA k K) : ↑(ell k K D) ≥ deg k K D + 1 - ↑(genus k K)

theorem MarkoffRiemannRoch.FunctionField.Chart.defect_le (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 : DivisorA k K) : defect k K D ≤ ↑(genus k K)

theorem MarkoffRiemannRoch.FunctionField.Chart.exists_defect_eq (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 : DivisorA k K), defect k K D = ↑(genus k K)

theorem MarkoffRiemannRoch.FunctionField.Chart.genus_le_of_family (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] (B C : DivisorA k K) (c₀ : ℤ) (hmono : ∀ (r : ℕ), defect k K (C + r • B) ≤ c₀) (hgrow : ∀ (m : ℤ), ∃ (r : ℕ), m ≤ ↑(ell k K (C + r • B))) : ↑(genus k K) ≤ c₀

Riemann's inequality along a growing pole family: the genus is at most c₀.

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.indexOfSpecialty (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 : DivisorA k K) : ℕ

The index of specialty i(D) = ℓ(D) − (deg D + 1 − g).

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.indexOfSpecialty_eq (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 : DivisorA k K) : ↑(indexOfSpecialty k K D) = ↑(ell k K D) - (deg k K D + 1 - ↑(genus k K))

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.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 : DivisorA k K) : ℕ

finrank k (A_K ⧸ (A(D) + diag(K))).

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.polar_deg_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] {x : K} (hx : ¬IsAlgebraic k x) : 0 < deg k K (polarDivisor k K x)

theorem MarkoffRiemannRoch.FunctionField.Chart.genus_ratFunc (k : Type u_1) [Field k] : genus k (RatFunc k) = 0

The genus of the rational function field RatFunc k is zero.