noncomputable def genus_data_ax {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] : { g : ℕ // (∀ (D : P →₀ ℤ), riemannDefect k D ≤ ↑g - 1) ∧ ∃ (D₀ : P →₀ ℤ), riemannDefect k D₀ = ↑g - 1 }

Axiomatized package of genus data for a function field $F/k$ with the chosen structure: a natural number $g \in \mathbb{N}$ together with the two defining properties of the genus, namely that the Riemann defect of every divisor is bounded above by $g - 1$ and that this bound is attained by at least one divisor $D_0$.

noncomputable def genusVal_ax {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] : ℕ

The genus value extracted from genus_data_ax: the unique $g$ such that $\max_D \mathrm{riemannDefect}(D) = g - 1$.

theorem riemannDefect_le_ax {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 →₀ ℤ) : riemannDefect k D ≤ ↑(genusVal_ax k) - 1

For every divisor $D$, the Riemann defect $r(D)$ is bounded above by $g - 1$, where $g$ is the genus extracted from genus_data_ax.

theorem genus_attained_ax {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 →₀ ℤ), riemannDefect k D₀ = ↑(genusVal_ax k) - 1

The genus bound is attained: there exists a divisor $D_0$ with $r(D_0) = g - 1$.

theorem dvf_ord_nonneg_of_mem_valuationSubring {F : Type u_1} [Field F] {P : Type u_2} {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (p : P) (x : F) (hx : x ∈ O p) : FunctionFieldAdeleRing.DiscreteValuationFamily.ord k p x ≥ ↑0

Axiomatized: an element of the valuation subring at $p$ has nonnegative order at $p$.

theorem dvf_ord_ne_top_of_ne_zero {F : Type u_1} [Field F] {P : Type u_2} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (p : P) (x : F) (hx : x ≠ 0) : FunctionFieldAdeleRing.DiscreteValuationFamily.ord k p x ≠ ⊤

A nonzero element of $F$ has finite order at every place $p$.

theorem dvf_ord_eq_coe_of_ne_zero {F : Type u_1} [Field F] {P : Type u_2} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (p : P) (x : F) (hx : x ≠ 0) : ∃ (n : ℤ), FunctionFieldAdeleRing.DiscreteValuationFamily.ord k p x = ↑n

For a nonzero $x \in F$, the order $\mathrm{ord}_p(x)$ is given by a (finite) integer.

theorem adele_covering_ax {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] (α : FunctionFieldAdeleRing F P O) (D : P →₀ ℤ) : ∃ (D' : P →₀ ℤ), (∀ (p : P), D p ≤ D' p) ∧ α ∈ AF_subspace k ⇑D'

Adele covering: any adele $\alpha \in \mathbb{A}_F$ and divisor $D$ admit a divisor $D' \ge D$ such that $\alpha$ lies in the adele subspace $A(D')$. The covering divisor is built from the component-wise orders of $\alpha$ together with the cofinite vanishing of its negative parts.

theorem riemannDefect_mono {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 D' : P →₀ ℤ) (h : ∀ (p : P), D p ≤ D' p) : riemannDefect k D ≤ riemannDefect k D'

Monotonicity of the Riemann defect: if $D \le D'$ pointwise, then $r(D) \le r(D')$.

theorem riemannDefect_le_of_genus {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 →₀ ℤ) : riemannDefect k D ≤ ↑(genusVal_ax k) - 1

Restatement of the genus bound riemannDefect_le_ax inside the Lemma22_10 section.

theorem adele_in_AF_of_restricted_product {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] (α : FunctionFieldAdeleRing F P O) (D : P →₀ ℤ) : ∃ (D' : P →₀ ℤ), (∀ (p : P), D p ≤ D' p) ∧ α ∈ AF_subspace k ⇑D'

Convenience restatement of adele_covering_ax: every adele is captured by some adele subspace $A(D')$ with $D' \ge D$.

theorem submodule_eq_of_finrank_quotient_zero {R : Type u_4} [DivisionRing R] {M : Type u_5} [AddCommGroup M] [Module R M] (S T : Submodule R M) (hST : S ≤ T) [hFD : FiniteDimensional R (↥T ⧸ Submodule.comap T.subtype S)] (h0 : Module.finrank R (↥T ⧸ Submodule.comap T.subtype S) = 0) : S = T

Linear-algebra lemma: if $S \le T$ are submodules of $M$ over a division ring with finite $T/S$ of dimension $0$, then $S = T$.

theorem AF_subspace_eq_top {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 →₀ ℤ) (hrD : riemannDefect k D = ↑(genusVal_ax k) - 1) : AF_subspace k ⇑D = ⊤

Lemma 22.10: if the Riemann defect of $D$ equals $g - 1$ (i.e. attains the maximum), then the adele subspace $A(D)$ exhausts the entire adele ring: $A(D) = \mathbb{A}_F$. Equivalently, $A = A(D) + F$ in the original formulation. The proof combines the covering lemma with the finite-quotient identification $S = T$ when their quotient has dimension $0$.