Unramifiedness at a prime of torsion Galois representations #
Definition: FLTPrelim_Ramification (2f679d60-0c74-5493-b36f-16da20baed9a), by Claude,
2026-09-05.
Three auxiliary notions and one instantiation. First, for a valuation subring $A$ of a field $L$ and
a natural number $q$, ValuationSubring.LiesOverPrime A q
says simply that the image of $q$ in $L$ lies in A.nonunits, i.e. $q$ belongs to the maximal ideal
of $A$; no primality of $q$ is required by the definition. Second, for an extension $L/K$,
ValuationSubring.inertiaSubgroupIn K A is the image of
Mathlib's inertia subgroup A.inertiaSubgroup K (a subgroup of the decomposition subgroup, i.e. of
the stabiliser of $A$ in $L \simeq_{\mathrm{alg}[K]} L$) under the inclusion
(A.decompositionSubgroup K).subtype, so that inertia is presented as a subgroup of the full
automorphism group $L \simeq_{\mathrm{alg}[K]} L$ rather than of the decomposition subgroup.
Third, given a tower $R \to S \to K$ with $S$, $K$ fields and an affine Weierstrass curve $W'$ over
$R$, WeierstrassCurve.Affine.Point.GaloisRepUnramifiedAt S K W' n q asserts: for every valuation subring $A$ of $K$ with $q \in A.\mathrm{nonunits}$, every $\sigma$ in the inertia subgroup of $A$ over $S$ (viewed in $K \simeq_{\mathrm{alg}[S]} K$), and every $x$ in the $n$-torsion submodule Submodule.torsionBy ℤ (W'⁄K).Point n of the point group of the base change of $W'$ to $K$, one has $\sigma \bullet x = x$. The action $\sigma \bullet x$ of automorphisms on points is the one supplied by the project's
Galois-representation module. Thus the predicate is the triviality of inertia on $n$-torsion, stated
place by place rather than through a representation object.
Finally, FreyPackage.GaloisRepUnramifiedAt P q is this
predicate for $R = S = \mathbb{Q}$, $K = \overline{\mathbb{Q}}$, the curve P.freyCurve and $n = P.p$: the mod-$p$ representation on $\overline{\mathbb{Q}}$-points of the Frey curve killed by $p$
is unramified at $q$.
Relation to Mathlib. ValuationSubring.LiesOverPrime
and ValuationSubring.inertiaSubgroupIn are thin wrappers
around Mathlib's valuation-subring API (nonunits, inertiaSubgroup, decompositionSubgroup), the
latter only transporting Mathlib's inertia subgroup along the inclusion of the decomposition
subgroup. The unramifiedness predicates for torsion points of a Weierstrass curve are the project's
own; Mathlib has no such notion.
Where it is used. These predicates express the local conditions on the mod-$p$ representation attached to a Frey package at primes $q$ not dividing the relevant level, which are what the Serre-type level-lowering and irreducibility arguments consume. The Frey-package instance is the form in which the unramifiedness of $E[p]$ outside the primes of bad reduction and $p$ enters the main line of the argument.
<!-- Generated by add_prove2me_provenance.py -->
The image of q belongs to the maximal ideal of the valuation ring.
Equations
- A.LiesOverPrime q = (↑q ∈ A.nonunits)
Instances For
The inertia subgroup viewed inside the full group of automorphisms over K.
Equations
Instances For
Every inertia element at every valuation ring above q fixes all n-torsion points.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The action on the Frey curve's p-torsion is unramified at every valuation ring above q.