Documentation

TauCeti.FieldTheory.FunctionField.Differential.LocalComponent

Local components of a Weil differential #

A k-linear form ω on the repartition space A_F of an algebraic function field F / k can be evaluated on the repartitions supported at a single place: writing ι_P x for the repartition with the entry x at P and 0 everywhere else, the local component of ω at P is the k-linear form

ω_P : F → k, ω_P x = ω (ι_P x)

on F itself. When ω is a Weil differential the local components determine it, and they do so by a sum: for every repartition a, all but finitely many of the values ω_P (a P) vanish and

ω a = ∑_P ω_P (a P).

Applying this to the constant repartition of a function x ∈ F — which a Weil differential kills, being a linear form on A_F / (A_F(D) + F) — gives ∑_P ω_P (x) = 0, the abstract residue theorem: it is Stichtenoth's (1.45) for x = 1, and it holds over an arbitrary constant field, with no analysis and before any residue map has been constructed.

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definitions 1.7.1, Proposition 1.7.2 and the divisor-free half of Proposition 1.7.3(a). For a function field with exact constants, the nonvanishing of every local component of a nonzero differential, and hence the fact that one local component determines the differential, are proved in TauCeti.FieldTheory.FunctionField.Differential.LocalNonvanishing. The remaining statements of Section I.7 — that v_P (ω) is the largest bound its local component respects and the explicit generator of Ω_{k(x)} — need the divisor of a Weil differential.

The repartitions ι_P x themselves are built in TauCeti.FieldTheory.FunctionField.Repartition.Basic, next to the repartition space and its filtration, which are all they depend on.

Main definitions #

Main results #

References #

The local components #

source
noncomputable def TauCeti.repartitionDualComponent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (ω : Module.Dual k ↥(repartitionSpace k F)) (P : Place k F) :
Module.Dual k F

The local component ω_P at a place P of a k-linear form ω on the repartition space (Stichtenoth, Definition 1.7.1): the k-linear form x ↦ ω (ι_P x) on F.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.repartitionDualComponent_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (ω : Module.Dual k ↥(repartitionSpace k F)) (P : Place k F) (x : F) :
    (repartitionDualComponent ω P) x = ω ((singleRepartition P) x)

    The defining formula ω_P x = ω (ι_P x) of a local component.

    source
    theorem TauCeti.repartitionDualComponent_repartitionDualMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (ω : Module.Dual k ↥(repartitionSpace k F)) (P : Place k F) (x : F) :
    (repartitionDualComponent (((repartitionDualMul hF) f) ω) P) x = (repartitionDualComponent ω P) (f * x)

    The local components of a multiple of a linear form: (f · ω)_P x = ω_P (f x).

    This is not @[simp]: simp already proves it from repartitionDualComponent_apply, repartitionDualMul_apply_apply and repartitionMul_singleRepartition, so tagging it is a simp-normal-form violation that scripts/lint-env.sh rejects.

    source
    theorem TauCeti.repartitionDualComponent_repartitionDualMul_algebraMap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (c : k) (ω : Module.Dual k ↥(repartitionSpace k F)) (P : Place k F) (x : F) :
    (repartitionDualComponent (((repartitionDualMul hF) ((algebraMap k F) c)) ω) P) x = c • (repartitionDualComponent ω P) x

    The local components of a constant multiple of a linear form: (c · ω)_P x = c • ω_P x. This is the case of TauCeti.repartitionDualComponent_repartitionDualMul in which the scalar is a constant, where the multiplication can be pulled out of the linear form.

    source
    theorem TauCeti.repartitionDualComponent_apply_eq_zero_of_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialFiltration D) (P : Place k F) {x : F} (hx : P.valuation x ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)) :
    (repartitionDualComponent ω P) x = 0

    The local component at P of a Weil differential bounded by D kills the functions whose pole at P is bounded by D: such an x has ι_P x ∈ A_F(D), which ω kills.

    source
    theorem TauCeti.finite_support_repartitionDualComponent_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) (a : ↥(repartitionSpace k F)) :
    (Function.support fun (P : Place k F) => (repartitionDualComponent ω P) (↑a P)).Finite

    The sum ∑_P ω_P (a P) has finitely many nonzero terms: for every repartition a, the values ω_P (a P) of the local components of a Weil differential vanish at all but finitely many places P (Stichtenoth, Proposition 1.7.2). It says nothing about a single local component ω_P, which is a linear form on all of F and need not vanish anywhere.

    source
    theorem TauCeti.apply_eq_finsum_repartitionDualComponent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) (a : ↥(repartitionSpace k F)) :
    ω a = ∑ᶠ (P : Place k F), (repartitionDualComponent ω P) (↑a P)

    A Weil differential is the sum of its local components: ω a = ∑_P ω_P (a P), a sum with finitely many nonzero terms (Stichtenoth, Proposition 1.7.2).

    source
    theorem TauCeti.mem_weilDifferentialFiltration_iff_repartitionDualComponent_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) :
    ω ∈ weilDifferentialFiltration D ↔ ∀ (P : Place k F) (x : F), P.valuation x ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P) → (repartitionDualComponent ω P) x = 0

    A Weil differential is bounded by D exactly when its local components are: the pole order of ω at each place is a local condition, read off from ω_P alone.

    This is the half of Stichtenoth, Proposition 1.7.3(a) that does not mention the divisor (ω): the bound at P restricts ω_P to vanish on the functions whose pole at P is bounded by D, and conversely those vanishings force ω to kill A_F(D), since ω is the sum of its local components.

    source
    theorem TauCeti.finsum_repartitionDualComponent_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) (x : F) :
    ∑ᶠ (P : Place k F), (repartitionDualComponent ω P) x = 0

    The abstract residue theorem (Stichtenoth, (1.45)): the local components of a Weil differential sum to zero on every function of F.

    The constant repartition of x lies in the diagonal copy of F inside A_F, on which every Weil differential vanishes, and its entry at every place is x. Stichtenoth states the case x = 1; no hypothesis on the constant field k is needed, and no residue map has been constructed.

    source
    theorem TauCeti.eq_zero_iff_repartitionDualComponent_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ∈ weilDifferentialSpace k F) :
    ω = 0 ↔ ∀ (P : Place k F), repartitionDualComponent ω P = 0

    A Weil differential is determined by its local components: it vanishes exactly when all of them do.