The product formula for algebraic function fields

This file proves that the principal divisor of every nonzero function has degree zero. More precisely, for a function z transcendental over k, both its zero divisor and its pole divisor have degree [F : k(z)]. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 1.4.11.

Here k is not assumed to be the exact constant field of F, so a function outside k may still be algebraic over k. Accordingly the hypothesis throughout is transcendence over k, which is strictly stronger than nonconstancy.

Main results

• TauCeti.Divisor.degree_zeros and TauCeti.Divisor.degree_poles compute the two effective parts of the principal divisor of a function transcendental over k.
• TauCeti.Divisor.degree_principal is the product formula.
• TauCeti.Place.finrank_adjoin_eq_mul_degree_of_ord_eq_neg: [F : k(z)] = n * deg P for a function z whose only pole is P, of order n.
• TauCeti.Divisor.succ_le_dim_nsmul_poles is the growth estimate for the powers of one transcendental function, ℓ(l (x)_∞) ≥ l + 1.
• TauCeti.Divisor.degreeClass descends degree to the divisor class group, with TauCeti.Divisor.ker_degreeClass_eq_picZero identifying its kernel Cl⁰(F) with the abstract Pic⁰, and TauCeti.Divisor.degree_eq_of_linearlyEquivalent records invariance under linear equivalence.
• TauCeti.riemannRochSpace_eq_bot_of_degree_neg and TauCeti.Divisor.dim_eq_zero_of_degree_neg are the negative-degree consequence, and TauCeti.Divisor.dim_le_degree_add_finrank_of_riemannRochSpace_ne_bot bounds ℓ(D) by deg D + [algebraicClosure k F : k] whenever L(D) is nonzero, and TauCeti.Divisor.exists_mem_dim_sub_ofPoint_lt shows that such an L(D) drops when some place of a set of sufficiently large total degree is removed.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.4.9, Theorem 1.4.11, and Corollary 1.4.12.

theorem TauCeti.Divisor.card_mul_succ_le_dim_nsmul_poles_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : Fˣ) (hx : Transcendental k ↑x) {ι : Type u_3} [Fintype ι] (c : ι → Fˣ) (hc : LinearIndependent ↥k⟮↑x⟯ fun (i : ι) => ↑(c i)) {C : Divisor k F} (hC : ∀ (i : ι), poles hF (c i) ≤ C) (l : ℕ) : Fintype.card ι * (l + 1) ≤ (l • poles hF x + C).dim

The growth estimate behind Stichtenoth's proofs of Theorems 1.4.11 and 1.4.14, in divisor form: if the functions c i are linearly independent over k⟮x⟯ and all their poles are dominated by one divisor C, then the #ι * (l + 1) products c i * x ^ j with j ≤ l are linearly independent elements of L(l (x)_∞ + C).

theorem TauCeti.Divisor.succ_le_dim_nsmul_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : Fˣ) (hx : Transcendental k ↑x) (l : ℕ) : l + 1 ≤ (l • poles hF x).dim

ℓ(l (x)_∞) ≥ l + 1 for a function x transcendental over k: the Riemann--Roch space of l times the pole divisor of x has dimension at least l + 1. Compared against Riemann--Roch in large degree, this is the lower bound behind the product formula and behind the vanishing of the genus of a rational function field.

@[simp]

theorem TauCeti.Divisor.degree_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hz : ¬IsAlgebraic k ↑z) : degree (poles hF z) = ↑(Module.finrank (↥k⟮↑z⟯) F)

Stichtenoth, Theorem 1.4.11: the pole divisor of a function z transcendental over k has degree [F : k(z)]. No exact-constant-field hypothesis is needed; correspondingly the hypothesis is transcendence over k, not mere nonconstancy.

@[simp]

theorem TauCeti.Divisor.degree_zeros {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (hz : ¬IsAlgebraic k ↑z) : degree (zeros hF z) = ↑(Module.finrank (↥k⟮↑z⟯) F)

Stichtenoth, Theorem 1.4.11: the zero divisor of a function z transcendental over k has degree [F : k(z)]. No exact-constant-field hypothesis is needed; correspondingly the hypothesis is transcendence over k, not mere nonconstancy.

@[simp]

theorem TauCeti.Divisor.degree_principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : degree (principal hF z) = 0

The product formula for an algebraic function field (Stichtenoth, Theorem 1.4.11): every principal divisor has degree zero.

theorem TauCeti.Place.isWeightedDegreeZero_orderSystem {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : (orderSystem hF).IsWeightedDegreeZero fun (P : Place k F) => ↑P.degree

The function-field order system satisfies the weighted degree-zero condition required to descend degree to divisor classes.

theorem TauCeti.Place.finrank_adjoin_eq_mul_degree_of_ord_eq_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {z : F} {P : Place k F} {n : ℕ} (hn : n ≠ 0) (hP : P.ord z = -↑n) (hQ : ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord z) : Module.finrank (↥k⟮z⟯) F = n * P.degree

The degree of the rational subfield generated by a function with a single pole: a function z with a pole of order n ≠ 0 at P that is regular at every other place has [F : k(z)] = n * deg P, the degree of its pole divisor nP (Stichtenoth, Theorem 1.4.11).

noncomputable def TauCeti.Divisor.degreeClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : (Place.orderSystem hF).ClassGroup →+ ℤ

The degree homomorphism on the divisor class group of an algebraic function field.

Equations

• TauCeti.Divisor.degreeClass hF = TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass (fun (P : TauCeti.Place k F) => ↑P.degree) ⋯

@[simp]

theorem TauCeti.Divisor.degreeClass_divisorClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : (degreeClass hF) ((Place.orderSystem hF).divisorClass D) = degree D

The degree of a divisor class is the degree of any representative.

theorem TauCeti.Divisor.ker_degreeClass_eq_picZero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : (degreeClass hF).ker = AlgebraicGeometry.WeilDivisor.OrderSystem.picZero (fun (P : Place k F) => ↑P.degree) ⋯

Cl⁰(F) is the abstract Pic⁰ of the function-field order system: the kernel of the degree map on divisor classes is the weighted-degree-zero part of the class group, for the residue-degree weights.

noncomputable def TauCeti.Divisor.degreeZeroClassHom {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : ↥degree.ker →+ ↥(degreeClass hF).ker

The degree-zero divisors map onto Cl⁰(F), a divisor going to its class. This is the order system's weightedDegreeZeroClassHom at the residue-degree weights, precomposed with the identification of the two degree-zero subgroups; no divisor-class reasoning is redone here.

Equations

• TauCeti.Divisor.degreeZeroClassHom hF = ((TauCeti.Place.orderSystem hF).weightedDegreeZeroClassHom (fun (P : TauCeti.Place k F) => ↑P.degree) ⋯).comp (AddSubgroup.inclusion ⋯)

@[simp]

theorem TauCeti.Divisor.coe_degreeZeroClassHom_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : ↥degree.ker) : ↑((degreeZeroClassHom hF) D) = (Place.orderSystem hF).divisorClass ↑D

The class of a degree-zero divisor is its divisor class, read in the full class group.

theorem TauCeti.Divisor.degreeZeroClassHom_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Function.Surjective ⇑(degreeZeroClassHom hF)

Every degree-zero class is the class of a degree-zero divisor. The surjectivity is the order system's, transported along the identification of the two degree-zero subgroups.

@[simp]

theorem TauCeti.Divisor.degreeZeroClassHom_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : ↥degree.ker} : (degreeZeroClassHom hF) D = 0 ↔ ∃ (z : Fˣ), principal hF z = ↑D

A degree-zero divisor has trivial class exactly when it is principal.

theorem TauCeti.Divisor.degree_eq_of_linearlyEquivalent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {A B : Divisor k F} (h : (Place.orderSystem hF).LinearlyEquivalent A B) : degree A = degree B

Linearly equivalent divisors have the same degree (Stichtenoth, Corollary 1.4.12(a)).

theorem TauCeti.riemannRochSpace_eq_bot_of_degree_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : Divisor.degree D < 0) : riemannRochSpace D = ⊥

A divisor of negative degree has no nonzero functions in its Riemann–Roch space (Stichtenoth, Corollary 1.4.12(b)).

theorem TauCeti.Divisor.dim_eq_zero_of_degree_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : degree D < 0) : D.dim = 0

A divisor of negative degree has Riemann–Roch dimension zero.

theorem TauCeti.Divisor.dim_le_degree_add_finrank_of_riemannRochSpace_ne_bot {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : riemannRochSpace D ≠ ⊥) : ↑D.dim ≤ degree D + ↑(Module.finrank k ↥(algebraicClosure k F))

A divisor with a nonzero Riemann–Roch space satisfies ℓ(D) ≤ deg D + [algebraicClosure k F : k] (Stichtenoth, Proposition 1.4.9 with Corollary 1.4.12(a)).

theorem TauCeti.Divisor.exists_mem_dim_sub_ofPoint_lt {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} {T : Finset (Place k F)} (hD : 0 < D.dim) (hdeg : degree D + ↑(Module.finrank k ↥(algebraicClosure k F)) < ↑D.dim + ∑ P ∈ T, ↑P.degree) : ∃ P ∈ T, (D - AlgebraicGeometry.WeilDivisor.ofPoint P).dim < D.dim

A nonzero Riemann–Roch space drops along a set of large degree. If ℓ(D) > 0 and the places of a finite set T have total degree exceeding deg D + [algebraicClosure k F : k] - ℓ(D), then removing some place of T strictly shrinks L(D). Over an exact constant field the threshold is deg D + 1 - ℓ(D).