The adele ring of a function field $F$ with set of places $P$ and valuation subrings $O_p \subseteq F$: the restricted product $\prod_{p \in P}' F$ of copies of $F$ with respect to the family $(O_p)$. An element $(\alpha_p)_{p \in P}$ is an adele iff $\alpha_p \in O_p$ for all but finitely many $p$.
Instances For
The adele ring inherits a commutative ring structure from the restricted product.
Adeles act as functions $P \to F$ via the underlying restricted product.
Two adeles are equal if they agree pointwise at every place.
The defining property of the adele ring: for any adele $\alpha$, $\alpha_p \in O_p$ for all but finitely many places $p$.
A subfield $k \subseteq F$ is called a field of constants for the family of valuation subrings $(O_p)$ if every element of $k$ is integral at every place $p$ and each residue field $O_p / \mathfrak{m}_p$ is finite-dimensional over $k$.
- residueField_finiteDimensional (p : P) : FiniteDimensional k (IsLocalRing.ResidueField ↥(O p))
Instances
Axiom: every constant $c \in k$ lies in $O_p$ at every place $p$.
Axiom: each residue field $O_p / \mathfrak{m}_p$ is a finite extension of $k$.
Instance bundling the two constant-field axioms.
The diagonal embedding $k \hookrightarrow \mathbb{A}_F$ sending a constant $c$ to the constant adele $(c, c, c, \dots)$.
Instances For
The $k$-algebra structure on the adele ring induced by the diagonal embedding.
Pointwise formula for the $k$-action on adeles: $(c \cdot \alpha)_p = c \cdot \alpha_p$.
Assumed: from a family $(O_p)_{p \in P}$ of valuation subrings of $F$ one obtains the function-field-curve structure on $P$ used elsewhere.
(Theorem 17.1.) A unit $f \in F^\times$ lies in the valuation subring $O_p$ if and only if its order at $p$ is non-negative: $f \in O_p \iff \operatorname{ord}_p(f) \ge 0$.
Convenience class bundling the function-field-curve hypothesis together with a chosen family of valuation subrings $O$.
- isCoordRingElem : Fˣ → Prop
- fraction_rep (f : Fˣ) : ∃ (g : Fˣ) (h : Fˣ), isCoordRingElem P g ∧ isCoordRingElem P h ∧ f = g * h⁻¹
Instances
Default instance deriving FunctionFieldProperty from a family of valuation subrings.
Every element of $F$ is integral at all but finitely many places, i.e. $f \in O_p$ for cofinitely many $p$. This is the integrality property that makes $F$ embed into the adele ring.
The diagonal $k$-linear embedding $F \hookrightarrow \mathbb{A}_F$ sending $f \mapsto (f, f, f, \dots)$.
Instances For
The submodule of principal adeles — the image of the diagonal embedding $F \hookrightarrow \mathbb{A}_F$.
Instances For
A discrete valuation family on $F$ over $k$: an assignment of an order function $\operatorname{ord}_p : F \to \mathbb{Z} \cup \{\infty\}$ to each $p \in P$ satisfying the usual discrete valuation axioms, with constants from $k$ having order zero and a uniformizer existing at every place.
Instances
Canonical instance assembling the order function and its axioms into a
DiscreteValuationFamily.
The adele subspace $\mathbb{A}_F(D) := \{\alpha \in \mathbb{A}_F : \operatorname{ord}_p(\alpha_p) \ge -D(p) \text{ for all } p\}$ associated to a $\mathbb{Z}$-valued divisor $D$.
Instances For
The space of Weil differentials on $D$: the annihilator in $\mathbb{A}_F^*$ of the subspace $\mathbb{A}_F(D) + F$. That is, $k$-linear functionals on $\mathbb{A}_F$ that vanish on both the adele subspace of $D$ and the principal adeles.
Instances For
The full Weil differential space $\Omega$ over $F$: the union $\bigcup_D \Omega(D)$ of Weil differentials over all divisors $D$.
Instances For
A linear-algebra identity: $\dim_k \Omega(D) = \dim_k (\mathbb{A}_F / (\mathbb{A}_F(D) + F))$, identifying Weil differentials at $D$ with the dual of the quotient space.
The complete data structure for a curve $C$ with function field $F$ and constant
subfield $k$ needed to prove Riemann-Roch: a CurveWithConstants together with all
ancillary structure used in the proof.
- isCoordRingElem : Fˣ → Prop
- fraction_rep (f : Fˣ) : ∃ (g : Fˣ) (h : Fˣ), isCoordRingElem C g ∧ isCoordRingElem C h ∧ f = g * h⁻¹
- const_isCoordRingElem (a : kˣ) : FunctionFieldCurve.isCoordRingElem C ((Units.map ↑(algebraMap k F)) a)
- const_inv_isCoordRingElem (a : kˣ) : FunctionFieldCurve.isCoordRingElem C ((Units.map ↑(algebraMap k F)) a)⁻¹
- residue_eval (P : C) : ∃ (evalP : F →ₗ[k] k), ∀ (f : Fˣ), CurveWithOrd.ord P f ≥ 0 → evalP ↑f = 0 → CurveWithOrd.ord P f ≥ 1
Instances
Axiom form: constants $c \in k^\times$ have order zero at every point $P \in C$.
Ultrametric inequality for sums of nonzero elements at a point: when $f + g \ne 0$, $\operatorname{ord}_P(f + g) \ge \min(\operatorname{ord}_P(f), \operatorname{ord}_P(g))$.
Axiom form: a unit $f \in F^\times$ with $\operatorname{ord}_P(f) = 0$ at every point $P \in C$ must be a constant, i.e. lies in the image of $k^\times \hookrightarrow F^\times$.
At every point $P$ of a curve there exists a uniformizer $\pi \in F^\times$ with $\operatorname{ord}_P(\pi) = 1$.
At every point $P$ there exists a $k$-linear "residue evaluation" map $\operatorname{ev}_P : F \to k$ such that any unit $f$ with non-negative order and vanishing residue actually has order $\ge 1$. This expresses that the residue map $O_P \to O_P/\mathfrak{m}_P \cong k$ is a $k$-linear functional.
The order at $P$ packaged as a multiplicative monoid homomorphism $F^\times \to \mathbb{Z}$ (written multiplicatively).
Instances For
Existence of a "residue functional at $P$" detecting the next divisor: there is a $k$-linear $\varphi : F \to k$ such that for any $f \in F^\times$, if $\operatorname{div}(f) + (D + P) \ge 0$ and $\varphi(f) = 0$ then in fact $\operatorname{div}(f) + D \ge 0$. This is the key tool used to bound $\ell(D + P) - \ell(D) \le 1$.
The residue functional packaged for use with the membership condition of the Riemann-Roch space (which handles both zero and nonzero elements).
Alias: constants have order zero at every point.
Short alias for RiemannRochData.ord_algebraMap_eq: constants have order zero.
Short alias: the ultrametric inequality $\operatorname{ord}_P(f+g) \ge \min(\operatorname{ord}_P f, \operatorname{ord}_P g)$ for nonzero $f+g$.
The degree of a principal divisor $\operatorname{div}(f)$ is zero.
A unit $f \in F^\times$ with $\operatorname{ord}_P(f) = 0$ at every point of $C$ is a constant from $k^\times$.
Public alias of the residue-evaluation functional (handles both zero and nonzero $f$).
The Riemann-Roch space $\mathcal{L}(D) := \{f \in F : f = 0 \text{ or } \operatorname{div}(f) + D \ge 0\}$, viewed as a $k$-subspace of $F$.
Instances For
Membership in $\mathcal{L}(D)$ unfolded: $f \in \mathcal{L}(D)$ iff $f = 0$ or $\operatorname{div}(f) + D$ is effective.
Membership in $\mathcal{L}(D)$ for a nonzero element simplifies to effectivity of $\operatorname{div}(f) + D$.
Multiplication by a unit $f$ with $\operatorname{div}(f) = A - B$ sends $\mathcal{L}(A)$ into $\mathcal{L}(B)$.
Multiplication by $f$ as a $k$-linear map $\mathcal{L}(A) \to \mathcal{L}(B)$ when $\operatorname{div}(f) = A - B$.
Instances For
If $\operatorname{div}(f) = A - B$ then $f \cdot - : \mathcal{L}(A) \cong \mathcal{L}(B)$ is a $k$-linear isomorphism, with inverse given by multiplication by $f^{-1}$.
Instances For
Linearly equivalent divisors have isomorphic Riemann-Roch spaces (existence form).
Monotonicity: if $A \le B$ then $\mathcal{L}(A) \subseteq \mathcal{L}(B)$.
Every divisor is bounded above by its positive part.
Helper: an effective divisor of degree zero is the zero divisor.
The Riemann-Roch space of the zero divisor is the field of constants: $\mathcal{L}(0) = k$.
$\mathcal{L}(0) = k \cdot 1$, the $k$-span of $1 \in F$.
$\mathcal{L}(0)$ is finite-dimensional over $k$ (it equals $k$).
$\ell(0) = \dim_k \mathcal{L}(0) = 1$.
Existence of the residue functional on $\mathcal{L}(D + P)$ whose kernel lies in $\mathcal{L}(D)$. This is the key ingredient for the inequality $\ell(D + P) \le \ell(D) + 1$.
Single-step bound: if $\mathcal{L}(D)$ is finite-dimensional then so is $\mathcal{L}(D + P)$, with $\ell(D + P) \le \ell(D) + 1$.
Comparison bound: if $A \le B$ and $\mathcal{L}(A)$ is finite-dimensional, then so is $\mathcal{L}(B)$ and $\ell(B) \le \ell(A) + \deg B - \deg A$.
Rearrangement of the comparison bound: $\ell(B) - \ell(A) \le \deg B - \deg A$ for $A \le B$.
For an effective divisor $D$, $\mathcal{L}(D)$ is finite-dimensional with $\ell(D) \le \deg D + 1$.
For an effective divisor $D$, $\mathcal{L}(D)$ is finite-dimensional.
For any divisor $D$, the Riemann-Roch space $\mathcal{L}(D)$ is finite-dimensional over $k$.
For any divisor $D$, $\ell(D) \le \deg(D^+) + 1$, where $D^+$ is the positive part.
The dimension $\ell(D) := \dim_k \mathcal{L}(D)$ of the Riemann-Roch space of a divisor $D$.
Instances For
Unfolds divisorDim to the dimension of the Riemann-Roch space.
$\ell(0) = 1$.
Linearly equivalent divisors have equal Riemann-Roch dimensions: $A \sim B$ implies $\ell(A) = \ell(B)$.
For $A \le B$, the difference of dimensions is bounded by the difference of degrees: $\ell(B) - \ell(A) \le \deg B - \deg A$.
Public alias: principal divisors have degree zero, $\deg(\operatorname{div}(f)) = 0$.
Public alias of the helper: an effective divisor of degree zero is the zero divisor.
A principal divisor $D = \operatorname{div}(f)$ has $\ell(D) = 1$ (it is linearly equivalent to $0$).
A non-principal divisor of degree zero has $\ell(D) = 0$: there is no nonzero $f \in F$ with $\operatorname{div}(f) + D$ effective.
For a divisor $D$ of degree zero, $\ell(D) = 1$ iff $D$ is principal.
$\mathcal{L}(D)$ is nonzero iff $D$ is linearly equivalent to an effective divisor.
Corollary 19.24 (axiomatised here): for an effective divisor $A$ there exists an effective $B$ such that for every $n$, $\mathcal{L}(nA + B)$ contains $(n+1) \deg A$ linearly independent elements over $k$.
Dimensional consequence of corollary_19_24: an effective $B$ exists such that
$\ell(nA + B) \geq (n+1) \deg A$ for every $n$. This is the lower-bound used to prove the
existence of the genus.
Existence of an effective "pole" divisor $A$ such that every effective $D$ is linearly equivalent to some $D' \leq nA$. Used to bound $\ell(D) - \deg D$ uniformly.
Combination of exists_pole_divisor_with_domination and
exists_basis_divisor_with_dim_bound: there exist effective divisors $A, B$ providing both
the domination property and the lower bound $\ell(nA + B) \geq (n+1) \deg A$.
A uniform genus bound for effective divisors: there exists a natural number $g$ with $\deg D + 1 - \ell(D) \leq g$ for all effective $D$. The genus is the least such $g$.
Genus bound for arbitrary divisors: there exists $g \in \mathbb{N}$ with
$\deg D + 1 - \ell(D) \leq g$ for every divisor $D$ (extending
exists_genus_bound_effective via the positive part).
The genus of the curve $C$: the least non-negative integer $g$ such that $\deg D + 1 - \ell(D) \leq g$ for every divisor $D$ (Theorem 22.3).
Instances For
The fundamental Riemann inequality: $\deg D + 1 - \ell(D) \leq g$ for every divisor $D$.
The genus is the least integer with the bound: if $g'$ also bounds $\deg D + 1 - \ell(D)$ for all $D$, then $g \leq g'$.
The genus bound is attained: there exists a divisor $D$ with $g = \deg D + 1 - \ell(D)$.
(Definition 22.1.) The integer $r(D) := \deg D - \ell(D)$ associated to a divisor $D$.
Instances For
Monotonicity of $r$: if $A \leq B$ then $r(A) \leq r(B)$.
Linearly equivalent divisors $A \sim B$ have the same $r$-value: $r(A) = r(B)$.
(Theorem 22.3, inequality.) For every divisor $D$, $r(D) \leq g - 1$.
(Theorem 22.3, equality.) For divisors of sufficiently large degree, $r(D) = g - 1$.
Axiomatic dimension-counting property used to prove $\dim_F \Omega = 1$ (Theorem 22.14): for any two nonzero $\omega_1, \omega_2$ in an $F$-module $\Omega$, there exist finite-dimensional $k$-subspaces $U_1, U_2$ of $F \cdot \omega_i$ whose individual dimensions grow like $n + \delta_i - g + 1$ but whose union has dimension at most $g - 1 + n$, forcing non-trivial intersection.
Instances For
Axiom: a nontrivial $F$-module of Weil differentials satisfies the dimension-counting property.
Axiom: if a module satisfies WeilDifferentialSubspaceData, then it is nontrivial.
For nonzero $\omega_1, \omega_2$ in a module satisfying WeilDifferentialSubspaceData,
there exist finite-dimensional $k$-subspaces $U_i \subseteq F \cdot \omega_i$ with
$\dim U_1 + \dim U_2 > \dim (U_1 \sqcup U_2)$, forcing $U_1 \cap U_2 \neq 0$.
If any two nonzero elements of $\Omega$ are $F$-proportional, then $\omega_2$ is an $F$-multiple of $\omega_1$ for all nonzero $\omega_1, \omega_2$.
An $F$-module with a nonzero element in which every two nonzero vectors are $F$-proportional has $F$-dimension one.
A nontrivial module of Weil differentials contains a nonzero element.
Convenience alias of dim_counting_property_of_axioms for the proof of Theorem 22.14.
Any two nonzero Weil differentials are $F$-proportional, i.e. there exist nonzero $f_1, f_2 \in F$ with $f_1 \omega_1 = f_2 \omega_2$.
(Theorem 22.14.) The space of Weil differentials $\Omega$ is one-dimensional over $F$: $\dim_F \Omega = 1$.
(Definition 22.4.) The index of speciality $i(D) := g - 1 - r(D) = g - \deg D - 1 + \ell(D)$ measuring how far the Riemann inequality is from equality.
Instances For
The index of speciality is non-negative: $i(D) \geq 0$.
Explicit formula: $i(D) = g - \deg D - 1 + \ell(D)$.
(Definition 22.16.) A divisor $W$ is canonical if $W = \operatorname{div}(\omega)$ for some
nonzero Weil differential $\omega$, witnessed by the existence of a divisor-of-differential
map divΩ realising $W$.
Instances For
The $k$-subspace $\Omega(D) := \{\omega \in \Omega : \operatorname{div}(\omega) \geq D\}$
of Weil differentials whose divisor dominates $D$. The hypotheses h_add and h_smul are
the standard valuation-style inequalities relating divΩ to the module structure.
Instances For
(Theorem 22.20.) The duality isomorphism $\mathcal{L}(W - D) \xrightarrow{\sim} \Omega(D)$ sending $f \in \mathcal{L}(W - D)$ to $f \cdot \omega_0$, where $\omega_0$ is a nonzero Weil differential with $\operatorname{div}(\omega_0) = W$.
Instances For
(Lemma 22.13, axiomatised.) The dimension of $\Omega(D)$ equals the index of speciality: $\dim_k \Omega(D) = i(D)$.
Given a canonical divisor $W$, exhibits the data of an $F$-module $\Omega$ of Weil
differentials with a distinguished nonzero element $\omega_0$ such that
$\operatorname{div}(\omega_0) = W$, satisfying all properties required by
duality_theorem_iso. Built concretely using $\Omega = F$ with $\omega_0 = 1$.
(Theorem 22.20, packaged form.) Duality: $i(D) = \ell(W - D)$ for any divisor $D$ and
canonical divisor $W$, obtained by combining duality_theorem_iso and
dim_differentialSpaceD_eq_indexOfSpeciality.
(Theorem 22.20.) The duality theorem: $i(D) = \ell(W - D)$.
(Theorem 22.21, The Riemann-Roch Theorem.) For a canonical divisor $W$ of a curve of genus $g$ and any divisor $D$: $\ell(D) = \deg D + 1 - g + \ell(W - D)$.
Riemann-Roch rearranged: $\ell(D) - \ell(W - D) = \deg D + 1 - g$.
(Part of Corollary 22.22.) For a canonical divisor $W$, $\ell(W) = g$.
(Part of Corollary 22.22.) For a canonical divisor $W$, $\deg W = 2g - 2$.
(Part of Corollary 22.22.) For a canonical divisor $W$, $i(W) = 1$.
(Corollary 21.11(e), one direction.) A divisor of negative degree has $\ell(D) = 0$.
(Corollary 22.23.) For divisors $D$ with $\deg D > 2g - 2$, $\ell(D) = \deg D + 1 - g$.
(Equivalent form of Corollary 22.23.) For $\deg D > 2g - 2$, $i(D) = 0$.
(Corollary 22.18.) Canonical divisors form a single linear equivalence class: if $W$ is canonical and $D$ is linearly equivalent to $W$ (i.e., $W - D$ is principal), then $D$ is canonical.
(Corollary 22.24, (a) implies (b).) If $D$ is canonical then $\ell(D) = g$ and $\deg D = 2g - 2$.
(Corollary 22.24, (b) implies (c).) If $\ell(D) = g$ and $\deg D = 2g - 2$, then $i(D) = 1$ and $\deg D$ is maximal among divisors with $i(D') = 1$.
(Corollary 22.24, (c) implies (a).) If $i(D) = 1$ and $\deg D$ is maximal among divisors of speciality $1$, then $D$ is canonical.
(Corollary 22.24, (a) iff (b).) $D$ is canonical iff $\ell(D) = g$ and $\deg D = 2g - 2$.
(Corollary 22.24, (a) iff (c).) $D$ is canonical iff $i(D) = 1$ and $\deg D$ is maximal among divisors with $i(D') = 1$.
(Corollary 22.24, full statement.) For a divisor $D$ of a genus $g$ curve admitting at least one canonical divisor, the three conditions are equivalent: (a) $D$ is canonical, (b) $\ell(D) = g$ and $\deg D = 2g - 2$, (c) $i(D) = 1$ with $\deg D$ maximal among divisors of speciality $1$.