@[reducible, inline]

noncomputable abbrev AF_subspace {F : Type u_1} [Field F] {P : Type u_2} {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (D : P → ℤ) : Submodule k (FunctionFieldAdeleRing F P O)

The $k$-subspace $A(D) + F \subseteq \mathbb{A}_F$: the sum of the adele divisor space $A(D)$ and the principal adeles (the image of $F$ embedded diagonally).

@[reducible, inline]

noncomputable abbrev LF_subspace {F : Type u_1} [Field F] {P : Type u_2} {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (D : P → ℤ) : Submodule k (FunctionFieldAdeleRing F P O)

The $k$-subspace $A(D) \cap F$ inside $\mathbb{A}_F$: elements of the function field that satisfy the divisor bounds at every place.

theorem AF_subspace_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] {A B : P → ℤ} (hAB : ∀ (p : P), A p ≤ B p) : AF_subspace k A ≤ AF_subspace k B

Monotonicity of the $A(D) + F$ subspaces in the divisor: $A \le B$ implies $A(A) + F \subseteq A(B) + F$.

noncomputable def rrSpaceAdele {F : Type u_1} [Field F] {P : Type u_2} {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] (D : P → ℤ) : Submodule k F

Riemann-Roch space $L(D) = \{f \in F \mid \mathrm{ord}_p(f) \ge -D(p) \text{ for all } p\}$ realized as the preimage of $A(D)$ under the diagonal embedding $F \hookrightarrow \mathbb{A}_F$.

theorem rrSpaceAdele_zero_le_constants {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] : rrSpaceAdele k 0 ≤ (Algebra.linearMap k F).range

For the zero divisor, $L(0)$ consists of constants: $L(0) \subseteq k$ (via the algebra map $k \hookrightarrow F$).

theorem rrSpaceAdele_zero_finiteDimensional {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] : FiniteDimensional k ↥(rrSpaceAdele k 0)

$L(0)$ is finite-dimensional over $k$: it is contained in the $k$-algebra-image of $k$ inside $F$.

theorem rrSpaceAdele_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) : rrSpaceAdele k D ≤ rrSpaceAdele k D'

Monotonicity of Riemann-Roch spaces: $D \le D'$ implies $L(D) \subseteq L(D')$.

theorem rrSpaceAdele_fd_step {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) (hFD_D : FiniteDimensional k ↥(rrSpaceAdele k ⇑D)) : FiniteDimensional k ↥(rrSpaceAdele k ⇑D')

Inductive step for finite-dimensionality of $L(D)$: if $L(D)$ is finite-dimensional and $D \le D'$, then $L(D')$ is finite-dimensional, using Lemma 22.8 to bound $L(D')/L(D)$ inside $A(D')/A(D)$.

theorem rrSpaceAdele_finiteDimensional {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 →₀ ℤ) : FiniteDimensional k ↥(rrSpaceAdele k ⇑D)

Lemma 22.9 (a). For any divisor $D$, the Riemann-Roch space $L(D)$ is finite-dimensional over the constant field $k$.

theorem diagonalLinearMap_injective {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] [Nonempty P] : Function.Injective ⇑(FunctionFieldAdeleRing.diagonalLinearMap k)

The diagonal embedding $F \hookrightarrow \mathbb{A}_F$ is injective when the set of places is nonempty.

theorem rrSpaceAdele_map_eq {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 → ℤ) : Submodule.map (FunctionFieldAdeleRing.diagonalLinearMap k) (rrSpaceAdele k D) = FunctionFieldAdeleRing.adeleSpace k D ⊓ FunctionFieldAdeleRing.principalAdeles k

Identification of $L(D)$ with $A(D) \cap F$ under the diagonal embedding: the image of $L(D)$ in $\mathbb{A}_F$ is precisely $A(D) \cap F$.

theorem LF_subspace_finiteDimensional {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] [Nonempty P] (D : P →₀ ℤ) : FiniteDimensional k ↥(FunctionFieldAdeleRing.adeleSpace k ⇑D ⊓ FunctionFieldAdeleRing.principalAdeles k)

$A(D) \cap F$ is finite-dimensional, as image of the finite-dimensional $L(D)$ under the injective diagonal embedding.

theorem LF_subspace_finrank {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] [Nonempty P] (D : P →₀ ℤ) : Module.finrank k ↥(FunctionFieldAdeleRing.adeleSpace k ⇑D ⊓ FunctionFieldAdeleRing.principalAdeles k) = Module.finrank k ↥(rrSpaceAdele k ⇑D)

Dimension equality: $\dim_k (A(D) \cap F) = \dim_k L(D)$, since the diagonal embedding restricts to a $k$-linear isomorphism.

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

The number $\ell(D) = \dim_k L(D)$, the $k$-dimension of the Riemann-Roch space attached to $D$.

theorem lemma_22_9_fd_LF_quotient {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] (A B : P →₀ ℤ) (hAB : ∀ (p : P), A p ≤ B p) : FiniteDimensional k (↥(FunctionFieldAdeleRing.adeleSpace k ⇑B ⊓ FunctionFieldAdeleRing.principalAdeles k) ⧸ Submodule.comap (FunctionFieldAdeleRing.adeleSpace k ⇑B ⊓ FunctionFieldAdeleRing.principalAdeles k).subtype (FunctionFieldAdeleRing.adeleSpace k ⇑A ⊓ FunctionFieldAdeleRing.principalAdeles k))

For $A \le B$, the quotient $(A(B) \cap F) / (A(A) \cap F)$ is finite-dimensional over $k$ (with the trivial case when $P$ is empty handled separately).

theorem lemma_22_9_finrank_LF_quotient {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] (A B : P →₀ ℤ) (hAB : ∀ (p : P), A p ≤ B p) : ↑(Module.finrank k (↥(FunctionFieldAdeleRing.adeleSpace k ⇑B ⊓ FunctionFieldAdeleRing.principalAdeles k) ⧸ Submodule.comap (FunctionFieldAdeleRing.adeleSpace k ⇑B ⊓ FunctionFieldAdeleRing.principalAdeles k).subtype (FunctionFieldAdeleRing.adeleSpace k ⇑A ⊓ FunctionFieldAdeleRing.principalAdeles k))) = ↑(ellD k B) - ↑(ellD k A)

Dimension of the LF-quotient: for $A \le B$, $$\dim_k \big((A(B) \cap F) / (A(A) \cap F)\big) = \ell(B) - \ell(A).$$

theorem finrank_sup_quotient_eq {R : Type u_4} [DivisionRing R] {M : Type u_5} [AddCommGroup M] [Module R M] (A B F_sub : Submodule R M) (hAB : A ≤ B) [hFD : FiniteDimensional R (↥B ⧸ Submodule.comap B.subtype A)] [hFD_inf : FiniteDimensional R (↥(B ⊓ F_sub) ⧸ Submodule.comap (B ⊓ F_sub).subtype (A ⊓ F_sub))] : FiniteDimensional R (↥(B ⊔ F_sub) ⧸ Submodule.comap (B ⊔ F_sub).subtype (A ⊔ F_sub)) ∧ Module.finrank R (↥(B ⊔ F_sub) ⧸ Submodule.comap (B ⊔ F_sub).subtype (A ⊔ F_sub)) + Module.finrank R (↥(B ⊓ F_sub) ⧸ Submodule.comap (B ⊓ F_sub).subtype (A ⊓ F_sub)) = Module.finrank R (↥B ⧸ Submodule.comap B.subtype A)

Modular-lattice / second-isomorphism dimension identity. For submodules $A \le B$ and any $F$ of a module $M$, the dimension of $(B + F)/(A + F)$ plus the dimension of $(B \cap F)/(A \cap F)$ equals the dimension of $B/A$, and finite-dimensionality is inherited.

theorem adeleDivisorDeg_add {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] (A B : P →₀ ℤ) : adeleDivisorDeg (A + B) = adeleDivisorDeg A + adeleDivisorDeg B

Additivity of divisor degree: $\deg(A + B) = \deg A + \deg B$.

theorem adeleDivisorDeg_sub {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] (A B : P →₀ ℤ) : adeleDivisorDeg (B - A) = adeleDivisorDeg B - adeleDivisorDeg A

Behavior of divisor degree under subtraction: $\deg(B - A) = \deg B - \deg A$.

noncomputable def riemannDefect {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 →₀ ℤ) : ℤ

The Riemann defect attached to a divisor $D$: $\delta(D) = \deg D + 1 - \ell(D)$, whose constant value (over varying $D$) is the genus $g$ in the Riemann-Roch theorem.

theorem AF_subspace_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] (A B : P →₀ ℤ) (hAB : ∀ (p : P), A p ≤ B p) : FiniteDimensional k (↥(AF_subspace k ⇑B) ⧸ Submodule.comap (AF_subspace k ⇑B).subtype (AF_subspace k ⇑A)) ∧ ↑(Module.finrank k (↥(AF_subspace k ⇑B) ⧸ Submodule.comap (AF_subspace k ⇑B).subtype (AF_subspace k ⇑A))) = riemannDefect k B - riemannDefect k A

Lemma 22.10. For divisors $A \le B$, the quotient $(A(B) + F) / (A(A) + F)$ is finite-dimensional over $k$ and its dimension is $\delta(B) - \delta(A)$, the difference of Riemann defects. Combines Lemmas 22.8 and 22.9 via the modular-lattice identity.