Documentation

TauCeti.FieldTheory.FunctionField.Repartition.Cokernel

The exact sequence of one step of the repartition filtration #

For divisors D ≤ E of an algebraic function field F / k the two subspaces A_F(D) + F and A_F(E) + F of the repartition space sit inside one another, and the quotient (A_F(E) + F) / (A_F(D) + F) is what measures the difference between the cokernels of A_F(D) + F → A_F and A_F(E) + F → A_F. This file computes that quotient, by exhibiting the exact sequence

0 → L(E)/L(D) → A_F(E)/A_F(D) → (A_F(E) + F)/(A_F(D) + F) → 0

as two explicit surjections and reading off ranks. The mathematics is the first step of Stichtenoth's proof of Theorem 1.5.4, and its input is the diagonal-intersection lemma TauCeti.diagonalRepartitions_inf_adeleFiltration (F ∩ A_F(D) = L(D)) in the relative form TauCeti.adeleFiltration_inf_sup_diagonalRepartitions (A_F(E) ∩ (A_F(D) + F) = A_F(D) + L(E)).

The exact sequence and its rank form need no finiteness; only the two ℓ-valued corollaries at the end assume IsFunctionField k F, for the finite-dimensionality of L(D) and L(E). Combined with the k-dimension deg E - deg D of A_F(E)/A_F(D), the rank identity below is the identity dim ((A_F(E) + F)/(A_F(D) + F)) = (deg E - ℓ(E)) - (deg D - ℓ(D)) that Stichtenoth uses to produce a divisor with A_F = A_F(D) + F and hence to identify the index of specialty i(D) with dim_k (A_F ⧸ (A_F(D) + F)).

Main definitions #

Main results #

Implementation notes #

Relative quotients are spelled ↥q ⧸ p.submoduleOf q with Mathlib's Submodule.submoduleOf, as in TauCeti.Place.filtration, so that they are meaningful without an inclusion p ≤ q. The subspace A_F(D) + F is written out as adeleFiltration D ⊔ diagonalRepartitions k F and not given a name of its own, since no result here needs one.

The right-hand map of the exact sequence gets no declaration: it is Noether's second isomorphism theorem, LinearMap.quotientInfEquivSupQuotient, applied to A_F(E) and A_F(D) + F, whose sup collapses to A_F(E) + F because A_F(D) ≤ A_F(E).

References #

The surjection L(E) → (A_F(E) ∩ (A_F(D) + F))/A_F(D) #

source
noncomputable def TauCeti.riemannRochSpaceToInfSupDiagonalQuotient {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) :
↥(riemannRochSpace E) →ₗ[k] ↥(adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F)) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F))

The composite L(E) ↪ A_F(E) ∩ (A_F(D) + F) ↠ (A_F(E) ∩ (A_F(D) + F))/A_F(D), the left-hand map of the exact sequence of this file: a function is sent to the class of its constant repartition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.riemannRochSpaceToInfSupDiagonalQuotient_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (f : ↥(riemannRochSpace E)) :
    (riemannRochSpaceToInfSupDiagonalQuotient D E) f = Submodule.Quotient.mk ⟨Function.const (Place k F) ↑f, ⋯⟩
    source
    theorem TauCeti.riemannRochSpaceToInfSupDiagonalQuotient_surjective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) :
    Function.Surjective ⇑(riemannRochSpaceToInfSupDiagonalQuotient D E)

    Every class of (A_F(E) ∩ (A_F(D) + F))/A_F(D) is represented by a constant, by the relative diagonal-intersection lemma.

    source
    theorem TauCeti.ker_riemannRochSpaceToInfSupDiagonalQuotient {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) :
    (riemannRochSpaceToInfSupDiagonalQuotient D E).ker = (riemannRochSpace D).submoduleOf (riemannRochSpace E)

    A function of L(E) has constant repartition in A_F(D) exactly when it lies in L(D), so the left-hand map of the exact sequence has kernel L(D).

    source
    noncomputable def TauCeti.riemannRochQuotientEquivInfSupDiagonalQuotient {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) :
    (↥(riemannRochSpace E) ⧸ (riemannRochSpace D).submoduleOf (riemannRochSpace E)) ≃ₗ[k] ↥(adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F)) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E ⊓ (adeleFiltration D ⊔ diagonalRepartitions k F))

    The left-hand map of the exact sequence, as an isomorphism: for D ≤ E, L(E)/L(D) ≅ (A_F(E) ∩ (A_F(D) + F))/A_F(D).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.riemannRochQuotientEquivInfSupDiagonalQuotient_apply_mk {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) (f : ↥(riemannRochSpace E)) :
      (riemannRochQuotientEquivInfSupDiagonalQuotient h) (Submodule.Quotient.mk f) = Submodule.Quotient.mk ⟨Function.const (Place k F) ↑f, ⋯⟩

      The rank identity #

      source
      theorem TauCeti.rank_quotient_adeleFiltration_eq_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (h : D ≤ E) :
      Module.rank k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E)) = Module.rank k (↥(riemannRochSpace E) ⧸ (riemannRochSpace D).submoduleOf (riemannRochSpace E)) + Module.rank k (↥(adeleFiltration E ⊔ diagonalRepartitions k F) ⧸ (adeleFiltration D ⊔ diagonalRepartitions k F).submoduleOf (adeleFiltration E ⊔ diagonalRepartitions k F))

      The exact sequence of one step of the filtration, in rank form (Stichtenoth, first step of the proof of Theorem 1.5.4): for D ≤ E,

      rank (A_F(E)/A_F(D)) = rank (L(E)/L(D)) + rank ((A_F(E) + F)/(A_F(D) + F)).

      No finiteness hypothesis is needed; the form that reads the middle term as ℓ(E) - ℓ(D) is TauCeti.rank_quotient_adeleFiltration_add_dim.

      source
      theorem TauCeti.rank_quotient_adeleFiltration_add_dim {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.rank k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E)) + ↑D.dim = Module.rank k (↥(adeleFiltration E ⊔ diagonalRepartitions k F) ⧸ (adeleFiltration D ⊔ diagonalRepartitions k F).submoduleOf (adeleFiltration E ⊔ diagonalRepartitions k F)) + ↑E.dim

      The exact sequence of one step of the filtration, with the Riemann–Roch quotient replaced by the dimensions it computes: for D ≤ E,

      rank (A_F(E)/A_F(D)) + ℓ(D) = rank ((A_F(E) + F)/(A_F(D) + F)) + ℓ(E).

      The identity is stated without subtraction because the two repartition quotients are only known to be finite once the degree count dim_k (A_F(E)/A_F(D)) = deg E - deg D is available.

      source
      theorem TauCeti.finiteDimensional_quotient_adeleFiltration_sup_diagonalRepartitions_iff {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)) ↔ FiniteDimensional k (↥(adeleFiltration E) ⧸ (adeleFiltration D).submoduleOf (adeleFiltration E))

      The two relative quotients of the exact sequence are finite-dimensional together: the Riemann–Roch quotient L(E)/L(D) between them is finite-dimensional for every divisor of an algebraic function field (TauCeti.finiteDimensional_riemannRochSpace).