Divisors of the rational function field

The rational function field k(x) is the base case of the theory of algebraic function fields, and this file computes its principal divisors: the divisor of an irreducible polynomial, its special case the divisor of x, and the degree of the pole divisor of a nonzero rational function. It continues the rational-function-field thread begun in TauCeti.FieldTheory.FunctionField.Place.RatFunc.Basic, where the places of k(x) are classified, and its Riemann–Roch consequences are TauCeti.FieldTheory.FunctionField.RiemannRoch.RatFunc.

Both calculations run on the classification of the places of k(x) together with the order computations of TauCeti.FieldTheory.FunctionField.Place.RatFunc.Order: an irreducible p has a simple zero at the place it defines, a pole of order deg p at infinity, and no other zeros or poles.

Main results

• TauCeti.Divisor.principal_irreducible: div p = P_(p) - (deg p) · P_∞ for p irreducible, and its special case TauCeti.Divisor.principal_X: div x = P_(X) - P_∞.
• TauCeti.Divisor.poles_X: the pole divisor of x is P_∞.
• TauCeti.Divisor.degree_poles_eq_max_natDegree: the pole divisor of z ∈ k(x)ˣ has degree max (deg z.num) (deg z.denom), which for nonconstant z is the degree of k(x) / k(z).

References

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

The divisor of an irreducible polynomial

theorem TauCeti.Divisor.principal_irreducible {k : Type u_1} [Field k] {p : Polynomial k} (hp : Irreducible p) : principal ⋯ (Units.mk0 ((algebraMap (Polynomial k) (RatFunc k)) p) ⋯) = AlgebraicGeometry.WeilDivisor.ofPoint (Place.adicOfIrreducible hp) - p.natDegree • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)

The divisor of an irreducible polynomial: div p = P_(p) - (deg p) · P_∞. An irreducible p has a simple zero at the finite place it defines, a pole of order deg p at infinity, and no other zeros or poles.

theorem TauCeti.Divisor.principal_X {k : Type u_1} [Field k] : principal ⋯ (Units.mk0 RatFunc.X ⋯) = AlgebraicGeometry.WeilDivisor.ofPoint (Place.adicOfIrreducible ⋯) - AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)

The divisor of x: div x = P_(X) - P_∞. The function x has a simple zero at the place of the polynomial X, a simple pole at infinity, and no other zeros or poles.

@[simp]

theorem TauCeti.Divisor.poles_X {k : Type u_1} [Field k] : poles ⋯ (Units.mk0 RatFunc.X ⋯) = AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)

The pole divisor of x: (x)_∞ = P_∞. The function x has a simple pole at infinity and is regular at every other place.

The degree of a rational map

theorem TauCeti.Divisor.degree_poles_eq_max_natDegree {k : Type u_1} [Field k] (z : (RatFunc k)ˣ) : degree (poles ⋯ z) = ↑(max (↑z).num.natDegree (↑z).denom.natDegree)

Stichtenoth, Theorem 1.4.11 on ℙ¹: the pole divisor of a nonzero rational function z ∈ k(x)ˣ has degree max (deg z.num) (deg z.denom). For nonconstant z this is [k(x) : k(z)], the degree of the covering ℙ¹ → ℙ¹ that z defines; a constant z = c is a unit at every place, and both sides are 0. A rational function is transcendental over k exactly when it is not a constant, by RatFunc.transcendental_of_ne_C.