Residue field as Fℓ and the reduction map reduceAt #
Definition: ValuationSubring_ReduceAt (b7b7698f-3b06-5e2c-b450-cbb382c3823b), by Claude,
2026-09-05.
Throughout, $L$ is a field and $A$ a valuation subring of $L$; A.LiesOverPrime q means that the
image of $q$ in $L$ lies in A.nonunits, i.e. $q$ is a non-unit of $A$, so that by
charP_residueField_of_liesOverPrime_def the residue field $\kappa(A) =$ ResidueField A has
characteristic $q$. Two groups of facts precede the main construction. First, field-theoretic ones:
if $L$ is algebraically closed then $\kappa(A)$ is algebraically closed (registered as an instance,
proved by lifting a monic irreducible polynomial to $A[X]$, finding a root in $L$, and using that a
valuation ring is integrally closed); under the same hypothesis, for $q$ prime with $A$ lying over
$q$, the $q$-power map on $\kappa(A)$ is bijective; if moreover $L$ has characteristic zero and is
algebraic over $\mathbb{Q}$, then every residue $\mathrm{res}_A(a)$, $a \in A$, is algebraic over
$\mathbb{Z}/\ell$, whence $\kappa(A)$ is an algebraic closure of $\mathbb{Z}/\ell$
(isAlgClosure_residueField). Second, integrality facts: for $\ell$ prime with $A$ lying over
$\ell$ and $n \in \mathbb{Z}$ with $\ell \nmid n$, the image of $n$ in $A$ is a unit and its residue
is non-zero; consequently $A$ lies over no prime $q \neq \ell$. A side lemma records that over a
nontrivial ring of prime characteristic every element is algebraic over $\mathbb{Z}$, the witness
being $\ell X$.
From isAlgClosure_residueField one obtains a ring equivalence residueFieldEquivAlgebraicClosure : ResidueField A ≃+* AlgebraicClosure (ZMod ℓ), chosen via the isomorphism of any two algebraic
closures and therefore not canonical. The main definition reduceAt A hA : L → AlgebraicClosure (ZMod ℓ) sends $a \in A$ to the image of $\mathrm{res}_A(a)$ under this equivalence and sends $a \notin A$ to $0$. It is thus not a ring homomorphism: the accompanying lemmas give
$\mathrm{reduceAt}(0)=0$, $\mathrm{reduceAt}(1)=1$, additivity and multiplicativity only for
arguments in $A$, surjectivity, the vanishing criterion $\mathrm{reduceAt}(a)=0 \iff a$ lies in the
maximal ideal of $A$ (for $a \in A$), compatibility with integer and natural-number casts,
$\mathrm{reduceAt}(\ell)=0$, and non-vanishing on integers prime to $\ell$.
Relation to Mathlib. Mathlib supplies ValuationSubring, IsLocalRing.ResidueField,
IsAlgClosure and AlgebraicClosure; the predicate LiesOverPrime and the total reduction
function reduceAt (defined to be $0$ off $A$) are the project's own, as is the instance that the
residue field of a valuation subring of an algebraically closed field is algebraically closed.
Where it is used. The function reduceAt A hA is the scalar-level reduction map at a place of
$\overline{\mathbb{Q}}$ above $\ell$ used in the specialisation of moduli coordinates and of points
of elliptic curves to the closed fibre, and hence in the comparison of inertia and Frobenius actions
entering the study of the mod-$p$ representation attached to a Frey package.
<!-- Generated by add_prove2me_provenance.py -->
Identify the residue field at a prime above ℓ with an algebraic closure of ZMod ℓ.
Equations
- A.residueFieldEquivAlgebraicClosure hA = (IsAlgClosure.equiv (ZMod ℓ) (IsLocalRing.ResidueField ↥A) (AlgebraicClosure (ZMod ℓ))).toRingEquiv
Instances For
Reduce an integral element into an algebraic closure of ZMod ℓ, returning zero for
nonintegral elements.
Equations
- A.reduceAt hA a = if h : a ∈ A then (A.residueFieldEquivAlgebraicClosure hA) ((IsLocalRing.residue ↥A) ⟨a, h⟩) else 0