The quotients of the divisor filtration of the repartition space

For two divisors D ≤ E of an algebraic function field F / k, the two steps A_F(D) and A_F(E) of the divisor filtration of the repartition space have a finite-dimensional quotient, of dimension

dim_k (A_F(E) / A_F(D)) = deg E - deg D

(TauCeti.finrank_quotient_adeleFiltration). This is the global half of the local-to-global engine of Stichtenoth's Section I.5, whose local half — the dimension (b - a) · deg P of a quotient 𝔪_P^a / 𝔪_P^b of two steps of the order filtration at a single place — is TauCeti.Place.finrank_quotient_filtration. It is the linear-algebra input of Stichtenoth's Theorem 1.5.4, which identifies the index of specialty i(D) with dim_k (A_F / (A_F(D) + F)), and through it of the one-dimensionality of the space of Weil differentials and of the Riemann–Roch theorem.

The two halves are joined one place at a time. When E - D is supported at a single place P, reading a repartition off at P is an isomorphism

A_F(E) / A_F(D) ≃ₗ[k] 𝔪_P^(-E P) / 𝔪_P^(-D P)

(TauCeti.adeleFiltrationQuotientEquiv): its kernel is A_F(D) because away from P the two bounds agree, and it is surjective because a function prescribed at P and extended by zero elsewhere is a repartition bounded by E. Running the same two arguments over a whole finite set s of places, one containing supp (E - D), identifies

A_F(E) / A_F(D) ≃ₗ[k] ⨁_{P ∈ s} 𝔪_P^(-E P) / 𝔪_P^(-D P)

(TauCeti.adeleFiltrationQuotientEquivPi); at s = supp (E - D) this is the local-to-global identification of Section I.5. The dimension count for a general pair D ≤ E is instead reached from the one-place case by walking up the finitely many places in the support of E - D, rank being additive along a tower of submodules (TauCeti.rank_quotient_submoduleOf_tower), which avoids having to sum the local dimensions.

Main definitions

• TauCeti.localFiltrationQuotient: the local quotient 𝔪_P^(-E P) / 𝔪_P^(-D P) at a place P.
• TauCeti.adeleFiltrationEval: evaluation of a repartition of A_F(E) at a place, landing in the step 𝔪_P^(-E P) of the order filtration there.
• TauCeti.adeleFiltrationLocalMap: that evaluation, read modulo 𝔪_P^(-D P).
• TauCeti.adeleFiltrationQuotientEquiv: the isomorphism A_F(E) / A_F(D) ≃ₗ[k] 𝔪_P^(-E P) / 𝔪_P^(-D P) for D and E agreeing away from P.
• TauCeti.adeleFiltrationLocalMapPi: the reduction read at every place of a finite set s at once, and TauCeti.adeleFiltrationQuotientLocalMapPi: the same map descended to A_F(E) / A_F(D).
• TauCeti.adeleFiltrationQuotientEquivPi: the isomorphism of A_F(E) / A_F(D) with the finite direct sum of the local quotients over s, for any s containing supp (E - D).

Main results

• TauCeti.ker_adeleFiltrationLocalMap and TauCeti.adeleFiltrationLocalMap_surjective: the local map has kernel A_F(D) — when the two divisors agree away from P — and is always surjective.
• TauCeti.ker_adeleFiltrationLocalMapPi and TauCeti.adeleFiltrationLocalMapPi_surjective: the same two facts for the reduction over s — the kernel as soon as s contains supp (E - D), the surjectivity for any s.
• TauCeti.rank_quotient_adeleFiltration: the rank form of the dimension formula, whose natural-number right-hand side carries the finiteness with it.
• TauCeti.finiteDimensional_quotient_adeleFiltration: the quotient is finite-dimensional.
• TauCeti.finrank_quotient_adeleFiltration: dim_k (A_F(E) / A_F(D)) = deg E - deg D.

Implementation notes

Relative quotients are spelled with Submodule.submoduleOf, as in TauCeti.Place.finrank_quotient_filtration and TauCeti.rank_quotient_submoduleOf_tower: A_F(D).submoduleOf (A_F(E)) is the trace of A_F(D) on A_F(E), which needs no inclusion A_F(D) ≤ A_F(E) to make sense. That is why the isomorphism above asks only that the two divisors agree away from P, and not that D ≤ E; the dimension count does need D ≤ E, since (b - a) · deg P is not the dimension of the trivial quotient obtained when b < a.

Mathlib has no mem_submoduleOf lemma. Since Submodule.submoduleOf is by definition a comap along the inclusion, membership in it is Submodule.mem_comap, which the proofs below cite in a show.

TauCeti.adeleFiltrationQuotientEquivPi descends to the quotient one factor at a time, as a LinearMap.pi of Submodule.liftQs, and is then turned into an equivalence by LinearEquiv.ofBijective. The direct route — Submodule.liftQ or LinearMap.quotKerEquivOfSurjective applied to TauCeti.adeleFiltrationLocalMapPi itself — elaborates a LinearMap whose codomain is a product of quotients, and the unifier does not finish that within the heartbeat limit; descending factorwise keeps every quotient it meets a single one.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.localFiltrationQuotient {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (P : Place k F) : Type u_2

The local quotient at a place P attached to two divisors D and E: the quotient 𝔪_P^(-E P) / 𝔪_P^(-D P) of two steps of the order filtration of F at P. Its dimension over k is (E P - D P) · deg P when D P ≤ E P (TauCeti.Place.finrank_quotient_filtration).

Equations

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

noncomputable def TauCeti.adeleFiltrationEval {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (E : Divisor k F) (P : Place k F) : ↥(adeleFiltration E) →ₗ[k] ↥(P.filtration (-AlgebraicGeometry.WeilDivisor.coeff E P))

Evaluation at a place P of the repartitions bounded by E: a repartition of A_F(E) has pole order at most E P at P, so its P-th entry lies in the step 𝔪_P^(-E P) of the order filtration of F at P.

Equations

• TauCeti.adeleFiltrationEval E P = LinearMap.codRestrict (P.filtration (-TauCeti.AlgebraicGeometry.WeilDivisor.coeff E P)) (LinearMap.proj P ∘ₗ (TauCeti.adeleFiltration E).subtype) ⋯

@[simp]

theorem TauCeti.coe_adeleFiltrationEval {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (E : Divisor k F) (P : Place k F) (a : ↥(adeleFiltration E)) : ↑((adeleFiltrationEval E P) a) = ↑a P

noncomputable def TauCeti.adeleFiltrationLocalMap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (P : Place k F) : ↥(adeleFiltration E) →ₗ[k] localFiltrationQuotient D E P

Reading a repartition of A_F(E) at the place P modulo 𝔪_P^(-D P), that is, modulo the bound that A_F(D) imposes there. When D and E agree away from P this map is exactly the projection of A_F(E) onto A_F(E) / A_F(D), which is TauCeti.adeleFiltrationQuotientEquiv.

Equations

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

@[simp]

theorem TauCeti.adeleFiltrationLocalMap_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (P : Place k F) (a : ↥(adeleFiltration E)) : (adeleFiltrationLocalMap D E P) a = Submodule.Quotient.mk ((adeleFiltrationEval E P) a)

theorem TauCeti.adeleFiltrationLocalMap_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (P : Place k F) (a : ↥(adeleFiltration E)) : (adeleFiltrationLocalMap D E P) a = 0 ↔ P.valuation (↑a P) ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D P)

The local reduction at P vanishes exactly when the bound that D imposes at P holds.

theorem TauCeti.ker_adeleFiltrationLocalMap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {P : Place k F} (hoff : ∀ (Q : Place k F), Q ≠ P → AlgebraicGeometry.WeilDivisor.coeff D Q = AlgebraicGeometry.WeilDivisor.coeff E Q) : (adeleFiltrationLocalMap D E P).ker = (adeleFiltration D).submoduleOf (adeleFiltration E)

The kernel of the local reduction at P is the trace of A_F(D) on A_F(E), as soon as the two divisors agree away from P: at every other place the bound imposed by D is the bound imposed by E, which every element of A_F(E) satisfies already.

theorem TauCeti.adeleFiltrationLocalMap_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (P : Place k F) : Function.Surjective ⇑(adeleFiltrationLocalMap D E P)

The local reduction at P is surjective: a function with pole order at most E P at P, extended by zero at every other place, is a repartition bounded by E.

noncomputable def TauCeti.adeleFiltrationQuotientEquiv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {P : Place k F} (hoff : ∀ (Q : Place k F), Q ≠ P → AlgebraicGeometry.WeilDivisor.coeff D Q = AlgebraicGeometry.WeilDivisor.coeff E Q) : (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E)) ≃ₗ[k] localFiltrationQuotient D E P

The local-to-global step: for two divisors agreeing away from a place P, reading a repartition off at P identifies A_F(E) / A_F(D) with the local quotient 𝔪_P^(-E P) / 𝔪_P^(-D P). This is the one-place case of Stichtenoth's computation of the quotients of the divisor filtration in Section I.5.

Equations

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

@[simp]

theorem TauCeti.adeleFiltrationQuotientEquiv_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {P : Place k F} (hoff : ∀ (Q : Place k F), Q ≠ P → AlgebraicGeometry.WeilDivisor.coeff D Q = AlgebraicGeometry.WeilDivisor.coeff E Q) (a : ↥(adeleFiltration E)) : (adeleFiltrationQuotientEquiv hoff) (Submodule.Quotient.mk a) = (adeleFiltrationLocalMap D E P) a

noncomputable def TauCeti.adeleFiltrationLocalMapPi {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (s : Finset (Place k F)) : ↥(adeleFiltration E) →ₗ[k] (P : ↥s) → localFiltrationQuotient D E ↑P

Reading a repartition of A_F(E) at each place of a finite set s of places, each entry taken modulo the bound that A_F(D) imposes there. The index set being finite, the target is the direct sum of the local quotients over s.

Equations

• TauCeti.adeleFiltrationLocalMapPi D E s = LinearMap.pi fun (P : ↥s) => TauCeti.adeleFiltrationLocalMap D E ↑P

@[simp]

theorem TauCeti.adeleFiltrationLocalMapPi_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (s : Finset (Place k F)) (a : ↥(adeleFiltration E)) (P : ↥s) : (adeleFiltrationLocalMapPi D E s) a P = (adeleFiltrationLocalMap D E ↑P) a

theorem TauCeti.ker_adeleFiltrationLocalMapPi {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {s : Finset (Place k F)} (hs : (E - D).support ⊆ s) : (adeleFiltrationLocalMapPi D E s).ker = (adeleFiltration D).submoduleOf (adeleFiltration E)

The kernel of the place-by-place reduction over s is the trace of A_F(D) on A_F(E), as soon as s contains the support of E - D: at every place outside that support the bound imposed by D is the bound imposed by E, which every element of A_F(E) satisfies already.

theorem TauCeti.adeleFiltrationLocalMapPi_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (s : Finset (Place k F)) : Function.Surjective ⇑(adeleFiltrationLocalMapPi D E s)

The place-by-place reduction over s is surjective: entries prescribed at the finitely many places of s, extended by zero elsewhere, form a repartition bounded by E.

noncomputable def TauCeti.adeleFiltrationQuotientLocalMapPi {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (s : Finset (Place k F)) : ↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E) →ₗ[k] (P : ↥s) → localFiltrationQuotient D E ↑P

The place-by-place reduction over s, descended to the quotient A_F(E) / A_F(D): it is well defined because a repartition bounded by D satisfies the bound D imposes at every place, so reduces to zero there.

Equations

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

@[simp]

theorem TauCeti.adeleFiltrationQuotientLocalMapPi_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (s : Finset (Place k F)) (a : ↥(adeleFiltration E)) (P : ↥s) : (adeleFiltrationQuotientLocalMapPi D E s) (Submodule.Quotient.mk a) P = (adeleFiltrationLocalMap D E ↑P) a

theorem TauCeti.adeleFiltrationQuotientLocalMapPi_bijective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {s : Finset (Place k F)} (hs : (E - D).support ⊆ s) : Function.Bijective ⇑(adeleFiltrationQuotientLocalMapPi D E s)

The descended place-by-place reduction is bijective as soon as s contains the support of E - D: injective by TauCeti.ker_adeleFiltrationLocalMapPi, surjective by TauCeti.adeleFiltrationLocalMapPi_surjective.

noncomputable def TauCeti.adeleFiltrationQuotientEquivPi {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {s : Finset (Place k F)} (hs : (E - D).support ⊆ s) : (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E)) ≃ₗ[k] (P : ↥s) → localFiltrationQuotient D E ↑P

The local-to-global identification (Stichtenoth, Section I.5): whenever a finite set s of places contains the support of E - D, reading a repartition of A_F(E) off at each place of s identifies

A_F(E) / A_F(D) ≃ₗ[k] ⨁_{P ∈ s} 𝔪_P^(-E P) / 𝔪_P^(-D P),

the index set s being finite, so that the product below is that direct sum. The smallest choice, and the one the local-to-global engine is usually stated with, is s = supp (E - D); its P-th component is TauCeti.adeleFiltrationLocalMap (TauCeti.adeleFiltrationQuotientEquivPi_mk).

Equations

• TauCeti.adeleFiltrationQuotientEquivPi hs = LinearEquiv.ofBijective (TauCeti.adeleFiltrationQuotientLocalMapPi D E s) ⋯

@[simp]

theorem TauCeti.adeleFiltrationQuotientEquivPi_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {s : Finset (Place k F)} (hs : (E - D).support ⊆ s) (a : ↥(adeleFiltration E)) (P : ↥s) : (adeleFiltrationQuotientEquivPi hs) (Submodule.Quotient.mk a) P = (adeleFiltrationLocalMap D E ↑P) a

theorem TauCeti.rank_quotient_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : Module.rank k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E)) = ↑(Divisor.degree E - Divisor.degree D).toNat

The rank of a quotient of the divisor filtration of the repartition space (Stichtenoth, Section I.5): for D ≤ E, the quotient A_F(E) / A_F(D) has rank deg E - deg D over k. The right-hand side is a natural number, so the statement carries the finite-dimensionality of the quotient with it (TauCeti.finiteDimensional_quotient_adeleFiltration).

theorem TauCeti.finiteDimensional_quotient_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : FiniteDimensional k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E))

The quotient of two steps of the divisor filtration of the repartition space is finite-dimensional.

theorem TauCeti.finrank_quotient_adeleFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (h : D ≤ E) : ↑(Module.finrank k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E))) = Divisor.degree E - Divisor.degree D

The dimension of a quotient of the divisor filtration of the repartition space (Stichtenoth, Section I.5): for D ≤ E,

dim_k (A_F(E) / A_F(D)) = deg E - deg D.

This is one of the two linear-algebra inputs to the later computation of the index of specialty, the other being the diagonal-intersection lemma F ∩ A_F(D) = L(D) (TauCeti.diagonalRepartitions_inf_adeleFiltration). Turning the two into i(D) = dim_k (A_F / (A_F(D) + F)) still needs the exact sequence relating L(E)/L(D), A_F(E)/A_F(D) and the cokernels of A_F(D) + F → A_F, which is not established here.