Principal divisors of an algebraic function field

The principal divisor of a nonzero function z of an algebraic function field F / k is the finite formal sum

div z = ∑_P ord_P z · P

of its zeros and poles, weighted by their orders. It is a finite sum because a function of an algebraic function field has only finitely many zeros and poles (TauCeti.Place.finite_setOf_ord_ne_zero), and it is additive in z because ord_P is. This file constructs it, splits it into its zero and pole divisors, and characterizes the functions with trivial divisor as the constants. It is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definition 1.4.2. Its consequences for Riemann–Roch spaces are TauCeti.FieldTheory.FunctionField.RiemannRoch.Principal.

The formal side is not rebuilt: the group Divisor k F and its degree are TauCeti.FieldTheory.FunctionField.Divisor.Basic, and the passage from a family of order functions to principal divisors, the subgroup they form, and linear equivalence is the existing TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem API. What is new here is the order system of the places of a function field, and the function-field statements that need the places themselves.

Main definitions

• TauCeti.Place.orderSystem: the places of F / k with their order functions, as an OrderSystem on Additive Fˣ. Its finiteness condition is Stichtenoth, Corollary 1.3.4.
• TauCeti.Divisor.principal and TauCeti.Divisor.principalHom: div z for z : Fˣ, and its packaging as a group homomorphism Additive Fˣ →+ Divisor k F (Definition 1.4.2).
• TauCeti.Divisor.zeros and TauCeti.Divisor.poles: the zero divisor (z)₀ = (div z)⁺ and the pole divisor (z)_∞ = (div z)⁻ (Definition 1.4.2).

Main results

• TauCeti.Divisor.zeros_sub_poles: div z = (z)₀ - (z)_∞, with both parts effective.
• TauCeti.Divisor.poles_eq_natCast_zsmul_ofPoint_of_ord_eq_neg: a function with a single pole, of order n at P, has pole divisor nP.
• TauCeti.Divisor.principal_eq_zero_iff_mem_algebraicClosure: div z = 0 exactly when z is a constant, and TauCeti.Divisor.principal_eq_zero_iff: over an exact constant field, exactly when z ∈ kˣ.
• TauCeti.Divisor.exists_units_algebraMap_mul_of_principal_eq: over an exact constant field, two functions with the same divisor differ by a constant, and TauCeti.Divisor.exists_units_algebraMap_mul_of_principal_eq_of_isAlgClosed: likewise over an algebraically closed one.
• TauCeti.Divisor.linearlyEquivalent_iff: two divisors are linearly equivalent exactly when their difference is the divisor of a function (Definition 1.4.3).
• TauCeti.Divisor.mem_principalSubgroup_iff and TauCeti.Divisor.divisorClass_eq_zero_iff: the principal-subgroup and trivial-class predicates in terms of the divisor of a function.

Implementation notes

div is defined on Fˣ, not on F with a nonzero hypothesis, so its multiplicativity is packaged as the group homomorphism Additive Fˣ →+ Divisor k F. For a nonzero f : F the divisor is div (Units.mk0 f hf), and TauCeti.Divisor.coeff_principal reads its coefficients back as orders of the underlying function.

The function-field hypothesis IsFunctionField k F is an explicit argument rather than a typeclass, following the rest of this directory; it is what makes the support finite, so it cannot be avoided in the definition. Since it is a Prop, two spellings of it give the same divisor.

The degree of a principal divisor is not computed here: deg (div z) = 0 is the product formula (Stichtenoth, Theorem 1.4.11), which needs deg (z)₀ = [F : k(z)] and is separate work. Everything in this file is independent of it.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.4.

Provenance

exists_units_algebraMap_mul_of_principal_eq corresponds to const_of_projectiveDivisorOf_eq_zero in AINTLIB's HasseWeil/HasseBound/WeilPairing/Constancy.lean, which states it for plane curves.

noncomputable def TauCeti.Place.orderSystem {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : AlgebraicGeometry.WeilDivisor.OrderSystem (Place k F) (Additive Fˣ)

The places of an algebraic function field, as an order system. The points are the places, the group is Additive Fˣ, and the order at a place is ord_P. The finiteness condition is Stichtenoth, Corollary 1.3.4: a function has finitely many zeros and poles.

Equations

• TauCeti.Place.orderSystem hF = { ord := fun (P : TauCeti.Place k F) => P.ordAddMonoidHom, finite_support := ⋯ }

@[simp]

theorem TauCeti.Place.orderSystem_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (P : Place k F) (z : Fˣ) : ((orderSystem hF).ord P) (Additive.ofMul z) = P.ord ↑z

The principal divisor

noncomputable def TauCeti.Divisor.principalHom {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Additive Fˣ →+ Divisor k F

The principal-divisor homomorphism div : Fˣ →+ Divisor k F of an algebraic function field, in its additivized form (Stichtenoth, Definition 1.4.2).

Equations

• TauCeti.Divisor.principalHom hF = (TauCeti.Place.orderSystem hF).principalHom

noncomputable def TauCeti.Divisor.principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : Divisor k F

The principal divisor div z = ∑_P ord_P z · P of a nonzero function (Stichtenoth, Definition 1.4.2).

Equations

• TauCeti.Divisor.principal hF z = (TauCeti.Divisor.principalHom hF) (Additive.ofMul z)

@[simp]

theorem TauCeti.Divisor.principalHom_ofMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : (principalHom hF) (Additive.ofMul z) = principal hF z

theorem TauCeti.Divisor.principalHom_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Additive Fˣ) : (principalHom hF) z = principal hF (Additive.toMul z)

@[simp]

theorem TauCeti.Divisor.coeff_principal {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) : AlgebraicGeometry.WeilDivisor.coeff (principal hF z) P = P.ord ↑z

The coefficient of a place in div z is the order of z there.

theorem TauCeti.Divisor.mem_support_principal_iff {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} : P ∈ (principal hF z).support ↔ P.ord ↑z ≠ 0

@[simp]

theorem TauCeti.Divisor.principal_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : principal hF 1 = 0

theorem TauCeti.Divisor.principal_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (y z : Fˣ) : principal hF (y * z) = principal hF y + principal hF z

@[simp]

theorem TauCeti.Divisor.principal_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : principal hF z⁻¹ = -principal hF z

theorem TauCeti.Divisor.principal_div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (y z : Fˣ) : principal hF (y / z) = principal hF y - principal hF z

theorem TauCeti.Divisor.principal_zpow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (n : ℤ) : principal hF (z ^ n) = n • principal hF z

theorem TauCeti.Divisor.principalDivisor_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Additive Fˣ) : (Place.orderSystem hF).principalDivisor z = principal hF (Additive.toMul z)

The principal divisor of a function is the principal divisor of the order system of the places of F / k.

theorem TauCeti.Divisor.mem_principalSubgroup_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} : D ∈ (Place.orderSystem hF).principalSubgroup ↔ ∃ (z : Fˣ), principal hF z = D

A divisor belongs to the principal subgroup exactly when it is the divisor of a nonzero function.

theorem TauCeti.Divisor.divisorClass_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} : (Place.orderSystem hF).divisorClass D = 0 ↔ ∃ (z : Fˣ), principal hF z = D

A divisor has trivial divisor class exactly when it is the divisor of a nonzero function.

theorem TauCeti.Divisor.linearlyEquivalent_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {A B : Divisor k F} : (Place.orderSystem hF).LinearlyEquivalent A B ↔ ∃ (z : Fˣ), principal hF z = A - B

Linear equivalence, in terms of functions: two divisors are linearly equivalent exactly when their difference is the divisor of a function. This is the multiplicative reading of TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.LinearlyEquivalent for the order system of places (Stichtenoth, Definition 1.4.3).

theorem TauCeti.Divisor.principal_eq_zero_of_isAlgebraic {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) : principal hF z = 0

The divisor of a function algebraic over the constants is trivial: such a function has neither zeros nor poles.

theorem TauCeti.Divisor.principal_eq_zero_iff_mem_algebraicClosure {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : principal hF z = 0 ↔ ↑z ∈ algebraicClosure k F

A function has trivial divisor exactly when it is a constant. One direction is that constants are units at every place; the other is that a function lying in every valuation ring is algebraic over k (TauCeti.Place.mem_algebraicClosure_iff_forall_mem_integers).

theorem TauCeti.Divisor.principal_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (z : Fˣ) : principal hF z = 0 ↔ ∃ (c : k), (algebraMap k F) c = ↑z

Stichtenoth, Definition 1.4.2, over an exact constant field: div z = 0 exactly when z ∈ kˣ. This is where exactness of the constant field enters — over ℝ ⊆ ℂ(x) the function i has trivial divisor without being a constant of ℝ.

The zero divisor and the pole divisor

noncomputable def TauCeti.Divisor.zeros {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : Divisor k F

The zero divisor (z)₀ = (div z)⁺ of a nonzero function (Stichtenoth, Definition 1.4.2): its zeros, with multiplicities.

Equations

• TauCeti.Divisor.zeros hF z = (TauCeti.Divisor.principal hF z)⁺

noncomputable def TauCeti.Divisor.poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : Divisor k F

The pole divisor (z)_∞ = (div z)⁻ of a nonzero function (Stichtenoth, Definition 1.4.2): its poles, with multiplicities.

Equations

• TauCeti.Divisor.poles hF z = (TauCeti.Divisor.principal hF z)⁻

@[simp]

theorem TauCeti.Divisor.coeff_zeros {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) : AlgebraicGeometry.WeilDivisor.coeff (zeros hF z) P = max (P.ord ↑z) 0

@[simp]

theorem TauCeti.Divisor.coeff_poles {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) : AlgebraicGeometry.WeilDivisor.coeff (poles hF z) P = max (-P.ord ↑z) 0

theorem TauCeti.Divisor.mem_support_zeros_iff {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} : P ∈ (zeros hF z).support ↔ 0 < P.ord ↑z

A place lies in the support of the zero divisor exactly when it is a zero of z.

theorem TauCeti.Divisor.mem_support_poles_iff {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} : P ∈ (poles hF z).support ↔ P.ord ↑z < 0

A place lies in the support of the pole divisor exactly when it is a pole of z.

@[simp]

theorem TauCeti.Divisor.isEffective_zeros {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : AlgebraicGeometry.WeilDivisor.IsEffective (zeros hF z)

@[simp]

theorem TauCeti.Divisor.isEffective_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : AlgebraicGeometry.WeilDivisor.IsEffective (poles hF z)

theorem TauCeti.Divisor.zeros_sub_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : zeros hF z - poles hF z = principal hF z

The divisor of a function splits into its zeros and its poles: div z = (z)₀ - (z)_∞.

theorem TauCeti.Divisor.poles_eq_zeros_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : poles hF z = zeros hF z⁻¹

The poles of a function are the zeros of its inverse.

theorem TauCeti.Divisor.poles_eq_natCast_zsmul_ofPoint_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 : ℕ} (hP : P.ord ↑z = -↑n) (hQ : ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord ↑z) : poles hF z = ↑n • AlgebraicGeometry.WeilDivisor.ofPoint P

The pole divisor of a function with a single pole: a function of order -n at P, with n : ℕ, that is regular at every other place has pole divisor nP.

theorem TauCeti.Divisor.exists_units_algebraMap_mul_of_principal_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {y z : Fˣ} (h : principal hF y = principal hF z) : ∃ (c : kˣ), ↑y = (algebraMap k F) ↑c * ↑z

Two functions with the same divisor differ by a constant of the base field, over an exact constant field.

theorem TauCeti.Divisor.exists_units_algebraMap_mul_of_principal_eq_of_isAlgClosed {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : IsFunctionField k F) {y z : Fˣ} (h : principal hF y = principal hF z) : ∃ (c : kˣ), ↑y = (algebraMap k F) ↑c * ↑z

Two functions with the same divisor differ by a constant, over an algebraically closed constant field — which is exact, every element of F algebraic over k lying in k. This is the form the divisor construction of the Weil pairing works under.

theorem TauCeti.Divisor.support_zeros_disjoint_poles {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) : Disjoint (zeros hF z).support (poles hF z).support

Zeros and poles never meet: no place is both.