The index of specialty is the dimension of a repartition cokernel

For a divisor D of an algebraic function field F / k with exact constant field, the index of specialty i(D) = ℓ(D) - deg D - 1 + g counts exactly how far the repartitions bounded by D together with the constants fall short of all repartitions:

i(D) = dim_k (A_F ⧸ (A_F(D) + F)).

This is Stichtenoth's Theorem 1.5.4, the linear-algebra summit that turns the index of specialty into a k-dimension. It is the input to Lemma 1.5.7, dim_k Ω_F(D) = i(D), which is what makes the space of Weil differentials nonzero and eventually one-dimensional over F. Its case D = 0 is Corollary 1.5.5, g = dim_k (A_F ⧸ (A_F(0) + F)), which reads the genus off the same quotient.

The two ingredients are already on main: the exact sequence of one step of the filtration (TauCeti.rank_quotient_adeleFiltration_add_dim, in Repartition/Cokernel.lean) and the degree count dim_k (A_F(E)/A_F(D)) = deg E - deg D (TauCeti.rank_quotient_adeleFiltration, in Repartition/Quotient.lean). Together they say that one step of the filtration of cokernels has dimension i(D) - i(E); the work here is Stichtenoth's observation that this vanishes as soon as D and E have the same index of specialty, so that the filtration of A_F by the subspaces A_F(D) + F becomes constant in large degree — and therefore reaches A_F itself, since every repartition is bounded by some divisor.

Main results

• TauCeti.finrank_quotient_adeleFiltration_sup_diagonalRepartitions: one step of the filtration of cokernels, dim_k ((A_F(E) + F)/(A_F(D) + F)) = i(D) - i(E) for D ≤ E.
• TauCeti.exists_adeleFiltration_sup_diagonalRepartitions_eq_repartitionSpace: every divisor D is dominated by a divisor E with A_F(E) + F = A_F (Stichtenoth, in the proof of Theorem 1.5.4).
• TauCeti.finrank_quotient_repartitionSpace: Stichtenoth, Theorem 1.5.4, i(D) = dim_k (A_F ⧸ (A_F(D) + F)).
• TauCeti.finrank_quotient_repartitionSpace_zero: Stichtenoth, Corollary 1.5.5, g = dim_k (A_F ⧸ (A_F(0) + F)).
• TauCeti.adeleFiltration_sup_diagonalRepartitions_eq_repartitionSpace_iff: the divisors with A_F(D) + F = A_F are exactly the nonspecial ones.

Implementation notes

Relative quotients are spelled ↥q ⧸ p.submoduleOf q with Mathlib's Submodule.submoduleOf, and the subspace A_F(D) + F is written out as adeleFiltration D ⊔ diagonalRepartitions k F, both as in Repartition/Cokernel.lean. The cokernel A_F ⧸ (A_F(D) + F) is therefore the relative quotient of repartitionSpace k F by adeleFiltration D ⊔ diagonalRepartitions k F; it gets no name of its own here.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5 (Theorem 1.5.4 and Corollary 1.5.5).

One step of the filtration of cokernels

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

For D ≤ E the quotient (A_F(E) + F)/(A_F(D) + F) is finite-dimensional: the exact sequence of TauCeti.finiteDimensional_quotient_adeleFiltration_sup_diagonalRepartitions_iff compares it with A_F(E)/A_F(D), which has dimension deg E - deg D.

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

One step of the filtration of cokernels (Stichtenoth, in the proof of Theorem 1.5.4): for D ≤ E,

dim_k ((A_F(E) + F)/(A_F(D) + F)) = i(D) - i(E).

This is the exact sequence TauCeti.rank_quotient_adeleFiltration_add_dim read together with the degree count TauCeti.rank_quotient_adeleFiltration; the genus cancels between the two indices of specialty, so no hypothesis on the constant field is needed.

The filtration of cokernels is constant in large degree

theorem TauCeti.adeleFiltration_sup_diagonalRepartitions_eq_of_indexOfSpecialty_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (hF : IsFunctionField k F) (h : D ≤ E) (hi : D.indexOfSpecialty = E.indexOfSpecialty) : adeleFiltration D ⊔ diagonalRepartitions k F = adeleFiltration E ⊔ diagonalRepartitions k F

Two divisors D ≤ E with the same index of specialty give the same subspace A_F(D) + F of the repartition space: the step between them has dimension i(D) - i(E) = 0.

theorem TauCeti.exists_adeleFiltration_sup_diagonalRepartitions_eq_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (D : Divisor k F) : ∃ (E : Divisor k F), D ≤ E ∧ E.indexOfSpecialty = 0 ∧ adeleFiltration E ⊔ diagonalRepartitions k F = repartitionSpace k F

Every divisor is dominated by one whose repartitions and constants exhaust A_F (Stichtenoth, in the proof of Theorem 1.5.4): for every D there is E ≥ D with i(E) = 0 and A_F(E) + F = A_F.

Riemann's theorem provides an E ≥ D of large enough degree to be nonspecial; every further enlargement of E is nonspecial too, so by TauCeti.adeleFiltration_sup_diagonalRepartitions_eq_of_indexOfSpecialty_eq it does not enlarge A_F(E) + F, while every single repartition is bounded by some divisor.

Theorem 1.5.4

theorem TauCeti.finiteDimensional_quotient_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : FiniteDimensional k (↥(repartitionSpace k F) ⧸ (adeleFiltration D ⊔ diagonalRepartitions k F).submoduleOf (repartitionSpace k F))

The cokernel A_F ⧸ (A_F(D) + F) is finite-dimensional over k, without an exact constant-field hypothesis.

theorem TauCeti.finrank_quotient_repartitionSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (D : Divisor k F) : ↑(Module.finrank k (↥(repartitionSpace k F) ⧸ (adeleFiltration D ⊔ diagonalRepartitions k F).submoduleOf (repartitionSpace k F))) = D.indexOfSpecialty

The index of specialty as a dimension (Stichtenoth, Theorem 1.5.4):

i(D) = dim_k (A_F ⧸ (A_F(D) + F))

for every divisor D of an algebraic function field with exact constant field.

theorem TauCeti.finrank_quotient_repartitionSpace_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : Module.finrank k (↥(repartitionSpace k F) ⧸ (adeleFiltration 0 ⊔ diagonalRepartitions k F).submoduleOf (repartitionSpace k F)) = genus k F

The genus as a dimension (Stichtenoth, Corollary 1.5.5): g = dim_k (A_F ⧸ (A_F(0) + F)), the case D = 0 of Theorem 1.5.4, where ℓ(0) = 1 because the constant field is exact.

theorem TauCeti.adeleFiltration_sup_diagonalRepartitions_eq_repartitionSpace_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (D : Divisor k F) : adeleFiltration D ⊔ diagonalRepartitions k F = repartitionSpace k F ↔ D.indexOfSpecialty = 0

The divisors whose repartitions and constants exhaust A_F are exactly the nonspecial ones: A_F(D) + F = A_F iff i(D) = 0.