Structure capturing the residue-field surjection at each place. For each
place $p \in P$, degPlace p is the $k$-degree of the residue field
$\mathcal{O}_p / \mathfrak{m}_p$, and φ D p₀ is a surjective $k$-linear map
from $A(D+p_0)$ onto $\mathcal{O}_{p_0}/\mathfrak{m}_{p_0}$ whose kernel is
exactly $A(D)$ — packaging the ingredient needed for Lemma 22.8.
- degPlace : P → ℕ
- φ (D : P → ℤ) (p₀ : P) : ↥(FunctionFieldAdeleRing.adeleSpace k (Function.update D p₀ (D p₀ + 1))) →ₗ[k] Fin (degPlace k O p₀) → k
- φ_ker (D : P → ℤ) (p₀ : P) : (φ D p₀).ker = Submodule.comap (FunctionFieldAdeleRing.adeleSpace k (Function.update D p₀ (D p₀ + 1))).subtype (FunctionFieldAdeleRing.adeleSpace k D)
Instances
A uniformizer exists at every place: an element $t \in F$ with
$\mathrm{ord}_p(t) = 1$. Wrapper around the corresponding axiom in the
DiscreteValuationFamily interface.
The residue field $\mathcal{O}_p/\mathfrak{m}_p$ at a place $p$ is a $k$-algebra via the composition $k \to \mathcal{O}_p \twoheadrightarrow \mathcal{O}_p/\mathfrak{m}_p$.
For a function field over its constant subfield $k$, the residue field at any place $p$ is finite-dimensional over $k$.
The degree $\deg p = [\mathcal{O}_p / \mathfrak{m}_p : k]$ of a place $p$, defined as the $k$-dimension of the residue field.
Instances For
The degree of any place is strictly positive: $\deg p \ge 1$.
An element of nonnegative order at $p$ lies in the valuation subring $\mathcal{O}_p$.
Converse: every element of $\mathcal{O}_p$ has nonnegative order at $p$.
Characterization of the maximal ideal: for $x \in \mathcal{O}_p$, the residue of $x$ vanishes iff $\mathrm{ord}_p(x) \ge 1$.
Existence of a $k$-linear extension of the residue map: a $k$-linear map $\psi : F \to k^{\deg p_0}$ which on $\mathcal{O}_{p_0}$ vanishes exactly on the maximal ideal, and is surjective.
Instances For
Reformulation of the residue map in terms of $\mathrm{ord}_{p_0}$ instead of $\mathcal{O}_{p_0}$-membership: $\psi$ vanishes on $\{\mathrm{ord}_{p_0} \ge 1\}$, has trivial kernel intersected with $\{\mathrm{ord}_{p_0} \ge 0\}$ beyond that, and is surjective onto $k^{\deg p_0}$.
Instances For
Normalization: $\mathrm{ord}_p(1) = 0$.
Order of an integer power of a uniformizer: $\mathrm{ord}_p(t^m) = m$ whenever $\mathrm{ord}_p(t) = 1$ and $t \neq 0$.
Shifted residue map: a $k$-linear surjection
$\varphi : F \to k^{\deg p_0}$ which vanishes on $\{\mathrm{ord}_{p_0} \ge -n+1\}$,
detects $\mathrm{ord}_{p_0} \ge -n+1$ within $\{\mathrm{ord}_{p_0} \ge -n\}$,
and is surjective on $\{\mathrm{ord}_{p_0} \ge -n\}$. Obtained by multiplying
base_residue_map by $t^n$ for a uniformizer $t$.
Instances For
Construction of an adele supported at a single place: given $x \in F$ with $\mathrm{ord}_{p_0}(x) \ge -(D(p_0) + 1)$, there is an adele $\alpha \in A(D')$ (where $D' = D + p_0$) whose $p_0$-th component is $x$ and all other components are $0$.
$k$-linear projection of an adele onto its $p_0$-component: the map $\alpha \mapsto \alpha(p_0)$ from the adele ring to $F$.
Instances For
The composed surjection $A(D + p_0) \xrightarrow{\alpha \mapsto \alpha(p_0)} F \xrightarrow{\varphi} k^{\deg p_0}$ realizing the residue-field surjection at the place $p_0$.
Instances For
residueSurjectionMap is surjective: every vector in $k^{\deg p_0}$ is
hit by some adele in $A(D + p_0)$.
The kernel of residueSurjectionMap equals $A(D)$ pulled back to
$A(D + p_0)$: the residue-field surjection identifies
$A(D + p_0) / A(D) \cong k^{\deg p_0}$.
Canonical instance assembling the previous data into a
HasResidueFieldSurjection structure under the standard hypotheses of a
discrete-valuation family on a function field with constant field $k$.
Degree of a divisor $D = \sum n_p \cdot p$ as $\deg D = \sum_p n_p \cdot \deg p$.
Instances For
Chain formula for finrank of quotients of submodules: for $S \le T \le U$ in $M$, $$\dim_R(U/S) = \dim_R(T/S) + \dim_R(U/T),$$ and the left side is finite-dimensional when both summands are.
Monotonicity of adele spaces in the divisor: $A \le B$ pointwise implies $A(A) \subseteq A(B)$.
Pullback of $A(A)$ to $A(B)$ as a $k$-submodule: the comap of $A(A)$ along the inclusion $A(B) \hookrightarrow $ adeles.
Instances For
Single-step dimension: incrementing $D$ by one at the place $p_0$ enlarges $A(D)$ by exactly $\deg p_0$ many $k$-dimensions, i.e. $\dim_k A(D + p_0) / A(D) = \deg p_0$.
Strict decrease of the induction measure: subtracting one at any place
$p$ in the support of $B - A$ strictly decreases divisorDistance A B.
The comap of $A(D)$ in itself is the top submodule.
The quotient $M / \top$ is the zero module, hence has $R$-rank $0$.
Behavior of divisor degree under addition of a single place: $\deg(D + p) = \deg D + \deg p$.
Lemma 22.8. For divisors $A \le B$, the quotient $A(B) / A(A)$ is
finite-dimensional over $k$ and $$\dim_k \big(A(B) / A(A)\big) = \deg(B - A).$$
Proved by strong induction on divisorDistance, peeling off one place at a
time and combining adeleSpace_singleStep_finrank with the chain formula
finrank_comap_chain.