noncomputable def adeleIndexOfSpeciality {F : Type u_1} [Field F] {P : Type u_2} [DecidableEq P] {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.FunctionFieldProperty F P O] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] [HasResidueFieldSurjection P F k O] (D : P →₀ ℤ) : ℤ

Adèle-theoretic index of speciality of a divisor $D$: the difference $g - 1 - r(D)$ between the genus and the Riemann defect at $D$.

theorem exists_defect_eq_genus_ax' {F : Type u_4} [Field F] {P : Type u_5} [DecidableEq P] {O : P → ValuationSubring F} (k : Type u_6) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.FunctionFieldProperty F P O] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] [HasResidueFieldSurjection P F k O] : ∃ (D₀ : P →₀ ℤ), riemannDefect k D₀ = ↑(genusVal_ax k) - 1

There exists a divisor $D_0$ whose Riemann defect attains the maximum value $g - 1$, where $g$ is the genus of the function field.

theorem exists_maximal_defect {F : Type u_1} [Field F] {P : Type u_2} [DecidableEq P] {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.FunctionFieldProperty F P O] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] [HasResidueFieldSurjection P F k O] (D : P →₀ ℤ) : ∃ (D' : P →₀ ℤ), (∀ (p : P), D p ≤ D' p) ∧ riemannDefect k D' = ↑(genusVal_ax k) - 1

Given any divisor $D$, one can find a larger divisor $D' \geq D$ whose Riemann defect attains the maximum value $g - 1$.

noncomputable def quotientTopEquiv {R : Type u_4} [DivisionRing R] {M : Type u_5} [AddCommGroup M] [Module R M] (S T : Submodule R M) (hT : T = ⊤) (hST : S ≤ T) : (↥T ⧸ Submodule.comap T.subtype S) ≃ₗ[R] M ⧸ S

When $T = \top$ and $S \leq T$, the quotient $T / (T \cap S)$ is canonically linearly equivalent to $M / S$.

theorem speciality_eq_adele_quotient_dim {F : Type u_1} [Field F] {P : Type u_2} [DecidableEq P] {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.FunctionFieldProperty F P O] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] [HasResidueFieldSurjection P F k O] (D : P →₀ ℤ) : FiniteDimensional k (FunctionFieldAdeleRing F P O ⧸ AF_subspace k ⇑D) ∧ ↑(Module.finrank k (FunctionFieldAdeleRing F P O ⧸ AF_subspace k ⇑D)) = adeleIndexOfSpeciality k D

Theorem 22.11. The index of speciality $i(D)$ equals the $k$-dimension of the adèle quotient $A_F / (A_F(D) + F)$; in particular this quotient is finite-dimensional.