Two-dimensional residual Galois representations and their properties #

Definition: GaloisRep_Residual (9f203110-aa25-59ba-bd12-df090d83ea51), by Claude, 2026-09-05.

GaloisFactorsThroughFiniteLevel ρ, for a monoid homomorphism $\rho$ from $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) = \mathrm{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}})$ to any monoid, asserts the existence of an intermediate field $L$ of $\overline{\mathbb{Q}}/\mathbb{Q}$, finite-dimensional over $\mathbb{Q}$, such that $\rho\sigma = 1$ whenever $\sigma$ fixes $L$ pointwise; this replaces continuity for the Krull topology with a discrete target, stated without any topology. ResidualGaloisRep k, for a field $k$, bundles a carrier type V with an abelian group and $k$-module structure, a field finrank_eq recording $\dim_k V = 2$, a monoid homomorphism $\rho$ from $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ to $\mathrm{End}_k(V)$ (multiplicativity forces each $\rho\sigma$ to be invertible), and a field asserting GaloisFactorsThroughFiniteLevel for $\rho$. A Module.Finite instance is derived from the rank.

The predicates on $\rho :$ ResidualGaloisRep k are: IsUnramifiedAt ρ q, for an arbitrary natural number $q$ (no primality is assumed), saying that for every valuation subring $A$ of $\overline{\mathbb{Q}}$ with $q$ a nonunit of $A$, every element of the image of the inertia subgroup of $A$ over $\mathbb{Q}$ acts as the identity; IsAttachedTo ρ f φ, for a weight-two cusp form $f$ on $\Gamma_0(N)$ and a ring homomorphism $\varphi$ from the algebraic integers in $\mathbb{C}$ to $k$, saying that for every prime $\ell \nmid N$ with $\ell \neq 0$ in $k$, every valuation subring $A$ over $\ell$ and every $\sigma$ which is a Frobenius at $A$ for $\ell$ (in the decomposition group, acting on the residue field by $x \mapsto x^{\ell}$), the $\ell$-th $q$-expansion coefficient of $f$ is an algebraic integer $a$ and $\rho\sigma$ has characteristic polynomial $X^2 - \varphi(a)X + \ell$ — nothing is required at $\ell \mid N$ or at the residue characteristic, and unramifiedness is not implied; IsOdd, that $\det \rho(c) = -1$ for every involution $c \neq 1$ of $\overline{\mathbb{Q}}/\mathbb{Q}$; IsIrreducible, that every $k$-submodule stable under all $\rho\sigma$ is $0$ or $V$; and IsAbsolutelyIrreducible, irreducibility after base change to $\overline{k}$. baseChange k' forms $k' \otimes_k V$ with $\rho\sigma$ base-changed (same finite level), baseChangeAlong φ does so along a ring homomorphism.

Finally, WeierstrassCurve.residualGaloisRepOf W p hcard hker packages, for a Weierstrass curve $W$ over $\mathbb{Q}$ and a prime $p$, the Galois action on the $p$-torsion of $W(\overline{\mathbb{Q}})$ as a ResidualGaloisRep (ZMod p): the carrier is Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point p, the homomorphism is the action of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ on torsion points by functoriality of $W$-points, and the two arithmetic inputs — that the $p$-torsion has exactly $p^2$ elements (whence rank $2$ over $\mathbb{Z}/p$) and that the action factors through a finite level — are taken as hypotheses rather than proved here.

Relation to Mathlib. Mathlib has no notion of Galois representation; the structure and all of these predicates are the project's own, as is the Galois action on the torsion of the points of a Weierstrass curve. Mathlib supplies the ambient ingredients: decomposition and inertia subgroups of a valuation subring, CuspForm on congruence subgroups with its $q$-expansion, LinearMap.charpoly, LinearMap.det and LinearMap.baseChange.

Where it is used. These definitions are the interface through which the mod-$p$ representation attached to the $p$-torsion of the Frey curve is handled: irreducibility and oddness of that representation, its unramifiedness away from the bad primes, and its attachment to a weight-two cusp form on $\Gamma_0(N)$ are the hypotheses and conclusions of the modularity and level-lowering steps.

source

def GaloisFactorsThroughFiniteLevel {M : Type} [MulOneClass M] (ρ : Gal(AlgebraicClosure ℚ/ℚ) →* M) :

Prop

The Galois action factors through a finite intermediate extension of the rational numbers.

Equations

GaloisFactorsThroughFiniteLevel ρ = ∃ (L : IntermediateField ℚ (AlgebraicClosure ℚ)), FiniteDimensional ℚ ↥L ∧ ∀ (σ : Gal(AlgebraicClosure ℚ/ℚ)), (∀ x ∈ L, σ x = x) → ρ σ = 1

Instances For

source

structure ResidualGaloisRep (k : Type) [Field k] :

Type 1

A two-dimensional representation over the coefficient field whose Galois action factors through a finite level.

V : Type
The underlying vector space of the residual representation.
instAddCommGroup : AddCommGroup self.V
instModule : Module k self.V
finrank_eq : Module.finrank k self.V = 2
ρ : Gal(AlgebraicClosure ℚ/ℚ) →* Module.End k self.V
The Galois action on the underlying vector space.
factorsThroughFiniteLevel : GaloisFactorsThroughFiniteLevel self.ρ