The trace of repartitions along an extension of function fields

Let F' / k' be a finite extension of the algebraic function field F / k. Stichtenoth builds the cotrace of Weil differentials (Section III.4) from the repartitions of F' that are constant on the fibres of the restriction map, that is, whose entries at two places P', Q' of F' agree whenever P' and Q' lie over the same place of F. Such a repartition is a family indexed by the places of F itself, and its trace is taken entrywise:

(Tr α)_P = Tr_{F'/F} (α_P).

This file sets up that construction. The relative repartitions are the families β : Place k F → F' whose entries are integral over 𝒪_P at almost every place P; they are exactly the families whose pullback P' ↦ β (P'.restrict k F) is a repartition of F' / k' (TauCeti.comp_restrict_mem_repartitionSpace_iff), so they are Stichtenoth's fibre-constant repartitions, with the entries read at the places of F. The entrywise trace carries them to repartitions of F / k, and the main theorem is the estimate that makes the divisor of the cotrace computable:

β ∘ restrict ∈ A_{F'}(Con D + Diff(F'/F)) → Tr β ∈ A_F(D),

obtained place by place from the valuation criterion for the complementary module, TauCeti.Place.valuation_trace_le_exp. The trace is compatible with the diagonal embeddings and with multiplication by functions of F.

Main definitions

• TauCeti.relativeRepartitionSpace: the relative repartitions of F' / F.
• TauCeti.relativeRepartitionPullback: the pullback identifying relative repartitions with the fibre-constant repartitions of F' / k'.
• TauCeti.repartitionTrace: the entrywise trace Tr_{F'/F}, an F-linear map from the relative repartitions to A_F.

Main results

• TauCeti.comp_restrict_mem_repartitionSpace and TauCeti.comp_restrict_mem_repartitionSpace_iff: the pullback of a relative repartition is a repartition of F' / k'.
• TauCeti.relativeRepartitionPullback_injective: pullback faithfully identifies relative repartitions with its range.
• TauCeti.mem_range_relativeRepartitionPullback_iff: the range of pullback is exactly the fibre-constant repartitions; they form a k'-subspace containing the constants (TauCeti.smul_mem_range_relativeRepartitionPullback, TauCeti.const_mem_range_relativeRepartitionPullback).
• TauCeti.exists_sub_relativeRepartitionPullback_mem_adeleFiltration: every repartition of F' is fibre-constant modulo A_{F'}(B'), for any divisor B' of F'.
• TauCeti.repartitionTrace_mem_adeleFiltration: the trace estimate Tr (A_{F'/F} ∩ A_{F'}(Con D + Diff(F'/F))) ⊆ A_F(D).
• TauCeti.repartitionTrace_const and TauCeti.repartitionTrace_smul: the trace of a diagonal repartition is diagonal, and the trace is F-linear.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.4, Definition 3.4.5 and the proof of Theorem 3.4.6.

Relative repartitions

noncomputable def TauCeti.relativeRepartitionSpace (k : Type u) (F : Type v) (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] : Submodule k (Place k F → F')

The relative repartitions of F' / F: the families β : Place k F → F' whose entry at P is integral over the valuation ring 𝒪_P for all but finitely many places P of F / k.

Pulled back along the restriction of places, these are the repartitions of F' that are constant on the fibres over the places of F, the space written A_{F'/F} by Stichtenoth (Section III.4); see TauCeti.comp_restrict_mem_repartitionSpace_iff.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mem_relativeRepartitionSpace_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] {β : Place k F → F'} : β ∈ relativeRepartitionSpace k F F' ↔ ∀ᶠ (P : Place k F) in Filter.cofinite, IsIntegral (↥P.integers) (β P)

Membership in the relative repartitions, unfolded.

theorem TauCeti.smul_mem_relativeRepartitionSpace {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) (f : F) {β : Place k F → F'} (hβ : β ∈ relativeRepartitionSpace k F F') : f • β ∈ relativeRepartitionSpace k F F'

The relative repartitions are stable under multiplication by a function of F, which has only finitely many poles.

theorem TauCeti.const_mem_relativeRepartitionSpace {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (x : F') : Function.const (Place k F) x ∈ relativeRepartitionSpace k F F'

The constant families are relative repartitions: a function of F', which is integral over F, is integral over 𝒪_P at almost every place P.

Pulling relative repartitions back to F'

theorem TauCeti.comp_restrict_mem_repartitionSpace {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {β : Place k F → F'} (hβ : β ∈ relativeRepartitionSpace k F F') : (fun (P' : Place k' F') => β (Place.restrict k F P')) ∈ repartitionSpace k' F'

The pullback of a relative repartition is a repartition of F' / k': at a place P' over a place P at which β P is integral over 𝒪_P, the entry β P is regular at P', and only finitely many places lie over the finitely many exceptional P.

noncomputable def TauCeti.relativeRepartitionPullback (k : Type u) (k' : Type u') (F : Type v) (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] : ↥(relativeRepartitionSpace k F F') →ₗ[k] ↥(repartitionSpace k' F')

Pullback of relative repartitions along restriction of places, as a k-linear map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.relativeRepartitionPullback_apply {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (β : ↥(relativeRepartitionSpace k F F')) (P' : Place k' F') : ↑((relativeRepartitionPullback k k' F F') β) P' = ↑β (Place.restrict k F P')

Pullback evaluates a relative repartition at the restricted place.

theorem TauCeti.relativeRepartitionPullback_injective {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') : Function.Injective ⇑(relativeRepartitionPullback k k' F F')

Pullback along restriction of places is injective: every place downstairs has a place above it, so the pullback determines every entry of a relative repartition.

theorem TauCeti.comp_restrict_mem_repartitionSpace_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') {β : Place k F → F'} : (fun (P' : Place k' F') => β (Place.restrict k F P')) ∈ repartitionSpace k' F' ↔ β ∈ relativeRepartitionSpace k F F'

The relative repartitions are the fibre-constant repartitions of F': a family indexed by the places of F is a relative repartition exactly when its pullback to the places of F' is a repartition. The converse direction needs every place of F to have a place above it and 𝒪'_P to be the intersection of the valuation rings above P, hence the hypotheses on F' and on the constant fields.

theorem TauCeti.mem_range_relativeRepartitionPullback_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') (a : ↥(repartitionSpace k' F')) : a ∈ (relativeRepartitionPullback k k' F F').range ↔ ∀ (P' Q' : Place k' F'), Place.restrict k F P' = Place.restrict k F Q' → ↑a P' = ↑a Q'

The range of pullback is exactly the fibre-constant repartitions: an upstairs repartition comes from a relative repartition precisely when its values agree at places restricting to the same downstairs place.

theorem TauCeti.exists_sub_relativeRepartitionPullback_mem_adeleFiltration {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (a : ↥(repartitionSpace k' F')) (B' : Divisor k' F') : ∃ (β : ↥(relativeRepartitionSpace k F F')), ↑a - ↑((relativeRepartitionPullback k k' F F') β) ∈ adeleFiltration B'

Every repartition of F' is fibre-constant modulo A_{F'}(B') (Stichtenoth, proof of Theorem 3.4.6): for a repartition a of F' / k' and a divisor B' of F', some relative repartition β of F' / F has a - β ∘ restrict ∈ A_{F'}(B').

Only finitely many fibres contain a place where a is not bounded by B'; on each of them weak approximation provides one function of F' close enough to a at all the places of the fibre.

theorem TauCeti.smul_mem_range_relativeRepartitionPullback {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') (c : k') {a : ↥(repartitionSpace k' F')} (ha : a ∈ (relativeRepartitionPullback k k' F F').range) : c • a ∈ (relativeRepartitionPullback k k' F F').range

The fibre-constant repartitions of F' form a k'-subspace: multiplying a fibre-constant repartition by a constant of F' keeps it fibre-constant.

theorem TauCeti.const_mem_range_relativeRepartitionPullback {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') {a : ↥(repartitionSpace k' F')} (ha : ↑a ∈ diagonalRepartitions k' F') : a ∈ (relativeRepartitionPullback k k' F F').range

The constant repartitions of F' are fibre-constant.

The trace

noncomputable def TauCeti.relativeRepartitionMul (k : Type u) (F : Type v) (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) : F →ₐ[k] Module.End k ↥(relativeRepartitionSpace k F F')

Multiplication by functions of F on relative repartitions.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def TauCeti.relativeRepartitionSpaceModule {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) : Module F ↥(relativeRepartitionSpace k F F')

The natural F-module structure on relative repartitions. It is a definition rather than a global instance because it depends on the explicit function-field hypothesis.

Equations

• TauCeti.relativeRepartitionSpaceModule hF = Module.compHom (↥(TauCeti.relativeRepartitionSpace k F F')) (TauCeti.relativeRepartitionMul k F F' hF).toRingHom

@[instance_reducible]

noncomputable def TauCeti.repartitionSpaceModule {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Module F ↥(repartitionSpace k F)

The natural F-module structure on repartitions. It is a definition rather than a global instance because it depends on the explicit function-field hypothesis.

Equations

• TauCeti.repartitionSpaceModule hF = Module.compHom (↥(TauCeti.repartitionSpace k F)) (TauCeti.repartitionMul hF).toRingHom

@[simp]

theorem TauCeti.coe_relativeRepartitionSpaceModule_smul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) (f : F) (β : ↥(relativeRepartitionSpace k F F')) : ↑(f • β) = f • ↑β

Scalar multiplication for the natural F-module structure on relative repartitions is entrywise multiplication.

@[simp]

theorem TauCeti.coe_repartitionSpaceModule_smul {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (f : F) (a : ↥(repartitionSpace k F)) : ↑(f • a) = f • ↑a

Scalar multiplication for the natural F-module structure on repartitions is entrywise multiplication.

theorem TauCeti.trace_comp_mem_repartitionSpace {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] {β : Place k F → F'} (hβ : β ∈ relativeRepartitionSpace k F F') : (fun (P : Place k F) => (Algebra.trace F F') (β P)) ∈ repartitionSpace k F

The entrywise trace of a relative repartition is a repartition of F / k: the trace of an element integral over the integrally closed ring 𝒪_P lies in 𝒪_P.

noncomputable def TauCeti.repartitionTrace (k : Type u) (F : Type v) (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) : ↥(relativeRepartitionSpace k F F') →ₗ[F] ↥(repartitionSpace k F)

The trace of relative repartitions Tr_{F'/F}, taken entrywise (Stichtenoth, Section III.4): the F-linear map carrying a relative repartition β of F' / F to the repartition P ↦ Tr_{F'/F} (β P) of F / k.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.repartitionTrace_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (β : ↥(relativeRepartitionSpace k F F')) (P : Place k F) : ↑((repartitionTrace k F F' hF) β) P = (Algebra.trace F F') (↑β P)

The entries of the trace of a relative repartition are the traces of its entries.

theorem TauCeti.repartitionTrace_const {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (β : ↥(relativeRepartitionSpace k F F')) {x : F'} (hβ : ↑β = Function.const (Place k F) x) : ↑((repartitionTrace k F F' hF) β) = Function.const (Place k F) ((Algebra.trace F F') x)

The trace of a diagonal repartition is diagonal: the trace of the constant family at x is the constant family at Tr_{F'/F} x.

theorem TauCeti.repartitionTrace_smul {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (f : F) (β : ↥(relativeRepartitionSpace k F F')) : (repartitionTrace k F F' hF) ⟨f • ↑β, ⋯⟩ = ((repartitionMul hF) f) ((repartitionTrace k F F' hF) β)

The trace of repartitions is F-linear: the trace of f • β is f times the trace of β.

theorem TauCeti.repartitionTrace_mem_adeleFiltration {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') {D : Divisor k F} (β : ↥(relativeRepartitionSpace k F F')) (hβ : ↑((relativeRepartitionPullback k k' F F') β) ∈ adeleFiltration ((Divisor.conorm k' F') D + Divisor.different k' F' hF)) : ↑((repartitionTrace k F F' hF) β) ∈ adeleFiltration D

The trace estimate (Stichtenoth, proof of Theorem 3.4.6): if the pullback of a relative repartition β to F' lies in A_{F'}(Con D + Diff(F'/F)), then its trace lies in A_F(D). At each place P of F this is TauCeti.Place.valuation_trace_le_exp: the coefficient of Con D + Diff(F'/F) at a place P' over P is e(P' ∣ P) · D(P) + d(P' ∣ P).