Documentation

TauCeti.FieldTheory.FunctionField.Differential.RatFunc

The canonical Weil differential of the rational function field #

The space of Weil differentials of the rational function field k(x) is one-dimensional over k(x), so it has no canonical element until a normalization is chosen. Stichtenoth pins one down by prescribing its divisor and one value of one local component: there is exactly one Weil differential η of k(x) / k with

(η) = -2 · P_∞ and η_{P_∞} (x⁻¹) = -1,

and it is the differential written dx in the classical language, whose local components are the residues η_P (z) = res_P (z dx). This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.7.4.

The construction #

The genus of k(x) is zero, so -2 · P_∞ has degree 2g - 2 and lies in the canonical class (TauCeti.divisorClass_neg_two_zsmul_ofPoint_infty); every divisor of that class is the divisor of a nonzero Weil differential, which produces a differential ω with (ω) = -2 · P_∞. Since P_∞ is rational with uniformizer x⁻¹, the local-order characterization of TauCeti.repartitionDualComponent_uniformizer_zpow_ne_zero says that ω_{P_∞} does not kill (x⁻¹) ^ (2 - 1) = x⁻¹, so scaling ω by the constant -(ω_{P_∞} (x⁻¹))⁻¹ — which does not move the divisor — normalizes that value to -1. Uniqueness is one-dimensionality: a second such differential is c · η, the divisor condition forces div c = 0, hence c ∈ k by exactness of the constant field, and the normalization forces c = 1.

The local components #

The values of η on the powers of x are the residues of xⁿ dx, that is -1 for n = -1 and 0 otherwise. Three separate mechanisms produce them: for n ≤ -2 the bound (η) = -2 · P_∞ kills xⁿ at P_∞; for n = -1 it is the normalization; and for n ≥ 0 it is the abstract residue theorem ∑_P η_P (z) = 0, whose other summands vanish because xⁿ is then a polynomial, hence regular at every finite place.

Main definitions #

Main results #

References #

The canonical class of the rational function field #

source
theorem TauCeti.divisorClass_neg_two_zsmul_ofPoint_infty (k : Type u_2) [Field k] :
(Place.orderSystem ⋯).divisorClass (-2 • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) = canonicalClass ⋯ ⋯

-2 · P_∞ represents the canonical class of k(x): it has degree -2 = 2g - 2 for the genus g = 0 of the rational function field, and ℓ(-2 · P_∞) ≥ 0 = g is vacuous.

The differential η #

source
noncomputable def TauCeti.ratFuncWeilDifferential (k : Type u_2) [Field k] :
Module.Dual k ↥(repartitionSpace k (RatFunc k))

The canonical Weil differential of the rational function field (Stichtenoth, Proposition 1.7.4): the unique Weil differential η of k(x) / k with divisor -2 · P_∞ whose local component at P_∞ sends the uniformizer x⁻¹ to -1.

Classically it is the differential dx, and its local components are the residues η_P (z) = res_P (z dx); TauCeti.eq_ratFuncWeilDifferential is the uniqueness that makes the normalization meaningful.

Equations
Instances For
    source
    theorem TauCeti.ratFuncWeilDifferential_mem (k : Type u_2) [Field k] :
    ratFuncWeilDifferential k ∈ weilDifferentialSpace k (RatFunc k)

    η is a Weil differential of k(x) / k.

    source
    theorem TauCeti.isGreatest_ratFuncWeilDifferential (k : Type u_2) [Field k] :
    IsGreatest {D : Divisor k (RatFunc k) | ratFuncWeilDifferential k ∈ weilDifferentialFiltration D} (-2 • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k))

    (η) = -2 · P_∞, in the form saying that -2 · P_∞ is the greatest divisor bounding η (Stichtenoth, Proposition 1.7.4).

    source
    theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_inv_X (k : Type u_2) [Field k] :
    (repartitionDualComponent (ratFuncWeilDifferential k) (Place.infty k)) RatFunc.X⁻¹ = -1

    The normalization η_{P_∞} (x⁻¹) = -1 (Stichtenoth, Proposition 1.7.4).

    This is deliberately not @[simp]: TauCeti.repartitionDualComponent_apply already unfolds the left-hand side to η (ι_{P_∞} x⁻¹), so tagging it would violate simp-normal form.

    source
    theorem TauCeti.ratFuncWeilDifferential_ne_zero (k : Type u_2) [Field k] :
    ratFuncWeilDifferential k ≠ 0

    η is nonzero: its local component at P_∞ takes the value -1.

    source
    theorem TauCeti.weilDifferentialDivisor_ratFuncWeilDifferential (k : Type u_2) [Field k] :
    weilDifferentialDivisor ⋯ ⋯ ⋯ ⋯ = -2 • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)

    The divisor of the canonical Weil differential of k(x) is -2 · P_∞ (Stichtenoth, Proposition 1.7.4).

    source
    theorem TauCeti.eq_ratFuncWeilDifferential {k : Type u_1} [Field k] {ω : Module.Dual k ↥(repartitionSpace k (RatFunc k))} (hmem : ω ∈ weilDifferentialSpace k (RatFunc k)) (hgreat : IsGreatest {D : Divisor k (RatFunc k) | ω ∈ weilDifferentialFiltration D} (-2 • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k))) (hnorm : (repartitionDualComponent ω (Place.infty k)) RatFunc.X⁻¹ = -1) :
    ω = ratFuncWeilDifferential k

    Uniqueness in Stichtenoth, Proposition 1.7.4: a Weil differential of k(x) with divisor -2 · P_∞ whose local component at P_∞ sends x⁻¹ to -1 is η.

    This is what makes the normalization meaningful: the two conditions of TauCeti.ratFuncWeilDifferential pin down a single differential.

    The local components of η #

    source
    theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_of_ne_infty {k : Type u_1} [Field k] {P : Place k (RatFunc k)} (hP : P ≠ Place.infty k) {z : RatFunc k} (hz : z ∈ P.integers) :
    (repartitionDualComponent (ratFuncWeilDifferential k) P) z = 0

    The local components of η away from infinity kill every regular function: the divisor of η is supported at P_∞ alone, so η_P vanishes on the valuation ring of every other place (Stichtenoth, Proposition 1.7.4). Classically this says that z dx has no residue at a finite place at which z is regular.

    source
    theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_algebraMap {k : Type u_1} [Field k] (p : Polynomial k) :
    (repartitionDualComponent (ratFuncWeilDifferential k) (Place.infty k)) ((algebraMap (Polynomial k) (RatFunc k)) p) = 0

    A polynomial has no residue at infinity: η_{P_∞} (p) = 0 for every p ∈ k[X].

    Classically this says that p dx is a regular differential on the affine line, so its only residue — the one at infinity — must vanish.

    source
    theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_zpow (k : Type u_2) [Field k] (n : ℤ) :
    (repartitionDualComponent (ratFuncWeilDifferential k) (Place.infty k)) (RatFunc.X ^ n) = if n = -1 then -1 else 0

    The local components of η on the powers of x (Stichtenoth, Proposition 1.7.4): at the place at infinity, η_{P_∞} (xⁿ) = -1 for n = -1 and 0 otherwise — the residues of xⁿ dx.