The order filtration of a function field at a place

A place P of F / k filters F by the order of vanishing at P: for an integer a, zero together with the nonzero functions satisfying ord_P z ≥ a forms the k-subspace

𝔪_P^a = {z ∈ F | v_P z ≤ exp (-a)}

of F, decreasing in a. At a = 0 its membership condition is v_P z ≤ 1, that of the valuation ring 𝒪_P, and at a = 1 it is v_P z < 1, that of the maximal ideal 𝔪_P of 𝒪_P. For negative a it is the fractional ideal of functions with a pole of order at most -a, so the whole filtration lives inside F and no completion is taken.

This file constructs that filtration and computes its successive quotients. Multiplication by a function of order -a identifies 𝔪_P^a / 𝔪_P^(a + 1) with the residue field F_P (TauCeti.Place.filtrationQuotientEquivResidueField), and iterating this along the tower gives the dimension formula

dim_k (𝔪_P^a / 𝔪_P^b) = (b - a) · deg P for a ≤ b

(TauCeti.Place.finrank_quotient_filtration). This is the local half of the local-to-global engine of Stichtenoth's Section I.5: the global half identifies the quotient A_F(E) / A_F(D) of two members of the divisor filtration of the repartition space with a finite direct sum of these local quotients, and so computes dim_k (A_F(E) / A_F(D)) = deg E - deg D.

Main definitions

• TauCeti.Place.filtration: the subspace 𝔪_P^a ⊆ F.
• TauCeti.Place.filtrationResidue: for s of order -a, the k-linear evaluation 𝔪_P^a → F_P, z ↦ (s · z)(P).
• TauCeti.Place.filtrationQuotientEquivResidueField: the induced isomorphism 𝔪_P^a / 𝔪_P^(a + 1) ≃ₗ[k] F_P.

Main results

• TauCeti.Place.rank_quotient_filtration_add_one: one step of the filtration has the rank of the residue field.
• TauCeti.Place.mem_maximalIdeal_pow_iff_coe_mem_filtration: the positive part of the place filtration is the maximal-ideal filtration of the valuation ring.
• TauCeti.Place.finrank_quotient_filtration_add and TauCeti.Place.finrank_quotient_filtration: dim_k (𝔪_P^a / 𝔪_P^b) = (b - a) · deg P, in the form indexed by b = a + n with n : ℕ and in the integer form.
• TauCeti.Place.finiteDimensional_quotient_filtration: those quotients are finite-dimensional as soon as the residue field is, which for a function field is TauCeti.Place.finiteDimensional_residueField.

Implementation notes

Membership is stated multiplicatively, as v_P z ≤ exp (-a), and not in the unguarded additive form ord_P z ≥ a, which the junk value ord_P 0 = 0 would get wrong at a > 0: the additive carrier would not contain 0 at positive a and so would not be a subspace. This is the convention of TauCeti.riemannRochSpace and TauCeti.adeleFiltration, of which this filtration is the one-place shadow; TauCeti.Place.mem_filtration_iff_le_ord is the additive form, guarded by z ≠ 0.

The relative quotients are spelled ↥(P.filtration a) ⧸ (P.filtration b).submoduleOf (P.filtration a), using Mathlib's Submodule.submoduleOf for the trace of the smaller subspace on the larger one. The dimension formula is proved first as a statement about Module.rank, where it needs no finiteness hypothesis at all, and then transported to Module.finrank through Cardinal.toNat_mul; it therefore holds unconditionally, both sides being zero when the residue field is infinite-dimensional over k.

References

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

The filtration

noncomputable def TauCeti.Place.filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) : Submodule k F

The subspace 𝔪_P^a whose nonzero elements are the functions satisfying ord_P z ≥ a at P, for a an arbitrary integer: for a ≤ 0 it is the space of functions with a pole of order at most -a at P, and for a > 0 the a-th power of the maximal ideal of 𝒪_P.

The defining condition is the multiplicative v_P z ≤ exp (-a), which is junk-free at z = 0; TauCeti.Place.mem_filtration_iff_le_ord is the additive form.

Equations

• P.filtration a = Submodule.restrictScalars k (P.valuation.leSubmodule (WithZero.exp (-a)))

@[simp]

theorem TauCeti.Place.mem_filtration_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a : ℤ} {z : F} : z ∈ P.filtration a ↔ P.valuation z ≤ WithZero.exp (-a)

Membership in 𝔪_P^a, unfolded.

theorem TauCeti.Place.mem_filtration_iff_le_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a : ℤ} {z : F} (hz : z ≠ 0) : z ∈ P.filtration a ↔ a ≤ P.ord z

The additive form of membership in 𝔪_P^a. The nonvanishing hypothesis guards the junk value ord_P 0 = 0: the zero function lies in 𝔪_P^a for every a, whereas the inequality a ≤ ord_P 0 fails precisely when a > 0.

theorem TauCeti.Place.mem_filtration_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {z : F} : z ∈ P.filtration 0 ↔ z ∈ P.integers

𝔪_P^0 is the valuation ring of P.

theorem TauCeti.Place.mem_filtration_one_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {z : F} : z ∈ P.filtration 1 ↔ P.valuation z < 1

Membership in 𝔪_P^1 is the maximal-ideal condition v_P z < 1 (TauCeti.Place.mem_maximalIdeal_iff_valuation_lt_one): 𝔪_P^1 is the maximal ideal of 𝒪_P, seen inside F.

@[simp]

theorem TauCeti.Place.mem_maximalIdeal_pow_iff_coe_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) (x : ↥P.integers) : x ∈ IsLocalRing.maximalIdeal ↥P.integers ^ n ↔ ↑x ∈ P.filtration ↑n

The positive part of the order filtration is the maximal-ideal filtration of the valuation ring: an integral function belongs to 𝔪_P ^ n exactly when its image in the function field lies in P.filtration n, that is, when v_P(x) ≤ exp (-n).

theorem TauCeti.Place.residue_eq_iff_sub_mem_filtration_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {y z : ↥P.integers} : (IsLocalRing.residue ↥P.integers) y = (IsLocalRing.residue ↥P.integers) z ↔ ↑y - ↑z ∈ P.filtration 1

Two functions integral at P have the same value at P exactly when they differ by a function of positive order: 𝔪_P^1 is the maximal ideal of 𝒪_P, seen inside F.

theorem TauCeti.Place.filtration_antitone {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Antitone P.filtration

The filtration decreases: vanishing to higher order is a stronger condition.

theorem TauCeti.Place.mul_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a b : ℤ} {z w : F} (hz : z ∈ P.filtration a) (hw : w ∈ P.filtration b) : z * w ∈ P.filtration (a + b)

A function of order at least a and one of order at least b have a product of order at least a + b.

theorem TauCeti.Place.pow_sub_one_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a : ℤ} {u : F} (hu : u ∈ P.integers) (h : u - 1 ∈ P.filtration a) (n : ℕ) : u ^ n - 1 ∈ P.filtration a

A function integral at P and congruent to 1 to order a stays congruent to 1 to order a after being raised to a power.

theorem TauCeti.Place.mem_filtration_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (z : F) : z ∈ P.filtration (P.ord z)

A function lies in the step of the filtration cut out by its own order. At z = 0 this reads 0 ∈ 𝔪_P^0, the junk value ord_P 0 = 0 doing no harm.

The successive quotients

theorem TauCeti.Place.mul_mem_integers_of_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) {z : F} (hz : z ∈ P.filtration a) : s * z ∈ P.integers

Multiplying a function of order at least a by one of order -a lands in the valuation ring: the integrality behind the evaluation map TauCeti.Place.filtrationResidue.

noncomputable def TauCeti.Place.filtrationResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) : ↥(P.filtration a) →ₗ[k] P.ResidueField

Evaluation of s · z at P, for a fixed function s of order -a: a k-linear map from 𝔪_P^a to the residue field F_P, whose kernel is 𝔪_P^(a + 1) and which is surjective. It is the local form of the evaluation map in Stichtenoth's proof of Lemma 1.4.8.

Defining the map needs nothing beyond hs; it is only its kernel and its surjectivity (TauCeti.Place.ker_filtrationResidue, TauCeti.Place.filtrationResidue_surjective) that fail at s = 0, so those carry the nonvanishing hypothesis.

Equations

• TauCeti.Place.filtrationResidue hs = { toFun := fun (z : ↥(P.filtration a)) => (IsScalarTower.toAlgHom k (↥P.integers) P.ResidueField) ⟨s * ↑z, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Place.filtrationResidue_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (z : ↥(P.filtration a)) : (filtrationResidue hs) z = (IsLocalRing.residue ↥P.integers) ⟨s * ↑z, ⋯⟩

theorem TauCeti.Place.filtrationResidue_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (hs0 : s ≠ 0) (z : ↥(P.filtration a)) : (filtrationResidue hs) z = 0 ↔ ↑z ∈ P.filtration (a + 1)

The evaluation z ↦ (s · z)(P) vanishes exactly on the next step of the filtration.

theorem TauCeti.Place.ker_filtrationResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (hs0 : s ≠ 0) : (filtrationResidue hs).ker = (P.filtration (a + 1)).submoduleOf (P.filtration a)

The evaluation z ↦ (s · z)(P) kills exactly the next step of the filtration.

theorem TauCeti.Place.filtrationResidue_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (hs0 : s ≠ 0) : Function.Surjective ⇑(filtrationResidue hs)

Every residue is attained: z ↦ (s · z)(P) maps 𝔪_P^a onto the residue field.

noncomputable def TauCeti.Place.filtrationQuotientEquivResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (hs0 : s ≠ 0) : (↥(P.filtration a) ⧸ (P.filtration (a + 1)).submoduleOf (P.filtration a)) ≃ₗ[k] P.ResidueField

The local quotient of the order filtration. Multiplication by a function s of order -a, followed by evaluation at P, identifies 𝔪_P^a / 𝔪_P^(a + 1) with the residue field F_P as k-vector spaces.

Equations

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

@[simp]

theorem TauCeti.Place.filtrationQuotientEquivResidueField_apply_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {a : ℤ} {s : F} (hs : P.ord s = -a) (hs0 : s ≠ 0) (z : ↥(P.filtration a)) : (filtrationQuotientEquivResidueField hs hs0) (Submodule.Quotient.mk z) = (IsLocalRing.residue ↥P.integers) ⟨s * ↑z, ⋯⟩

The quotient equivalence evaluates the residue of s * z on a representative z.

theorem TauCeti.Place.rank_quotient_filtration_add_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) : Module.rank k (↥(P.filtration a) ⧸ (P.filtration (a + 1)).submoduleOf (P.filtration a)) = Module.rank k P.ResidueField

One step of the order filtration has the rank of the residue field.

theorem TauCeti.Place.rank_quotient_filtration_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) (n : ℕ) : Module.rank k (↥(P.filtration a) ⧸ (P.filtration (a + ↑n)).submoduleOf (P.filtration a)) = ↑n * Module.rank k P.ResidueField

The dimension of a local quotient of the order filtration, in the form indexed by a natural number of steps: dim_k (𝔪_P^a / 𝔪_P^(a + n)) = n · deg P, at the level of ranks and so without any finiteness hypothesis on the residue field.

theorem TauCeti.Place.finrank_quotient_filtration_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (a : ℤ) (n : ℕ) : Module.finrank k (↥(P.filtration a) ⧸ (P.filtration (a + ↑n)).submoduleOf (P.filtration a)) = n * P.degree

The dimension of a local quotient of the order filtration (Stichtenoth, Section I.5): the k-dimension of 𝔪_P^a / 𝔪_P^(a + n) is n · deg P.

Both sides are junk — zero — when the residue field is infinite-dimensional over k, so no finiteness hypothesis is needed; for a function field the residue field is always finite-dimensional (TauCeti.Place.finiteDimensional_residueField).

theorem TauCeti.Place.finrank_quotient_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {a b : ℤ} (hab : a ≤ b) : ↑(Module.finrank k (↥(P.filtration a) ⧸ (P.filtration b).submoduleOf (P.filtration a))) = (b - a) * ↑P.degree

The dimension of a local quotient of the order filtration, in integer form: for a ≤ b, dim_k (𝔪_P^a / 𝔪_P^b) = (b - a) · deg P. This is the local input of the local-to-global engine computing dim_k (A_F(E) / A_F(D)) = deg E - deg D for the divisor filtration of the repartition space.

theorem TauCeti.Place.finiteDimensional_quotient_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Module.Finite k P.ResidueField] (a b : ℤ) : FiniteDimensional k (↥(P.filtration a) ⧸ (P.filtration b).submoduleOf (P.filtration a))

The local quotients of the order filtration are finite-dimensional as soon as the residue field is, which for a function field is TauCeti.Place.finiteDimensional_residueField. No order relation between a and b is needed: for b ≤ a the quotient is trivial.