Rank-two Galois representations over a local coefficient ring

Definition: GaloisRep_Adic (4658c4b2-4079-5082-a13b-6de985889cee), by Claude, 2026-09-05.

Fix a commutative local ring $A$ with maximal ideal $\mathfrak m$. GaloisActionIsAdicContinuous A ρ, for a monoid homomorphism $\rho$ from $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$ (realised as $\overline{\mathbb Q}\simeq_{\mathbb Q}\overline{\mathbb Q}$, with $\overline{\mathbb Q}=$ AlgebraicClosure ℚ) to $\mathrm{End}_A(V)$, asserts: for every $n$ there is an intermediate field $L$ of $\overline{\mathbb Q}/\mathbb Q$, finite-dimensional over $\mathbb Q$, such that every $\sigma$ fixing $L$ pointwise satisfies $\rho(\sigma)v-v\in\mathfrak m^n\cdot V$ for all $v$. No topology on $A$, on $V$ or on the Galois group is used; this is the project's own substitute for continuity. A GaloisRepAdic A then bundles a type $V$ with an $A$-module structure that is free and finite, the equation $\operatorname{finrank}_A V=2$, a monoid homomorphism $\rho$ into $\mathrm{End}_A(V)$, and the above condition as a field.

For $\rho :$ GaloisRepAdic A: IsUnramifiedAt ρ q says that for every valuation subring $P$ of $\overline{\mathbb Q}$ lying over the prime $q$ (predicate LiesOverPrime, from an imported module), every element of P.inertiaSubgroupIn ℚ acts as the identity; det ρ is the character $\mathrm{Gal}\to A^\times$ obtained from $\sigma\mapsto\det(\rho(\sigma))$ via toHomUnits, and trace ρ σ is $\operatorname{tr}_A(\rho(\sigma))$. baseChangeAlong φ hφ transports $\rho$ along an explicit ring homomorphism $\varphi:A\to B$ of local rings that is assumed local, with carrier $B\otimes_A V$ and $\rho(\sigma)$ replaced by its base change; residual ρ is the representation on $\kappa\otimes_A V$, $\kappa$ the residue field of $A$, as a ResidualGaloisRep, its finite-level field being deduced from adic continuity for $n=1$.

Equivalence is data: Equiv ρ₁ ρ₂ consists of an $A$-linear isomorphism $e:V_1\to V_2$ together with the intertwining identity $e(\rho_1(\sigma)x)=\rho_2(\sigma)(e(x))$ for all $\sigma,x$; IsEquiv is its Nonempty. Helper declarations give reflexivity, symmetry, transitivity, compatibility of Equiv with base change and with passage to the residual representation, and, when the coefficients form a field $k$, mutually inverse passages between GaloisRepAdic k and ResidualGaloisRep k on the same carrier.

Relation to Mathlib. Mathlib has no notion of a Galois representation; the structures and the adic-continuity predicate are the project's own, built on Mathlib's Module.Free/Module.Finite, Module.finrank, LinearMap.det/LinearMap.trace, tensor-product base change, IsLocalRing.ResidueField and ValuationSubring.inertiaSubgroupIn. Change of coefficients is always along an explicit φ : A →+* B with an explicit IsLocalHom φ argument, never an ambient Algebra A B instance.

Where it is used. These are the coefficient-ring-valued two-dimensional representations used throughout the lifting argument: representations with values in a localised Hecke algebra, universal deformations of a residual representation, and Tate modules of elliptic curves over $p$-adic rings. The module supplies the currency (unramifiedness, trace and determinant, base change, reduction to the residue field, and equivalence) on which the deformation-theoretic and Hecke-algebra modules that import it are phrased.

<!-- Generated by add_prove2me_provenance.py -->

def GaloisActionIsAdicContinuous (A : Type) [CommRing A] [IsLocalRing A] {V : Type} [AddCommGroup V] [Module A V] (ρ : Gal(AlgebraicClosure ℚ/ℚ) →* Module.End A V) : Prop

At every maximal-ideal power, the action is trivial modulo that power on the subgroup fixing some finite extension of the rationals.

Equations

• One or more equations did not get rendered due to their size.

structure GaloisRepAdic (A : Type) [CommRing A] [IsLocalRing A] : Type 1

An adically continuous Galois representation on a finite free rank-two module over a local coefficient ring.

• V : Type

  The finite free rank-two module carrying the representation.

• instAddCommGroup : AddCommGroup self.V
• instModule : Module A self.V
• instFree : Module.Free A self.V
• instFinite : Module.Finite A self.V
• finrank_eq : Module.finrank A self.V = 2
• ρ : Gal(AlgebraicClosure ℚ/ℚ) →* Module.End A self.V

  The Galois action by linear endomorphisms of the coefficient module.

• isAdicContinuous : GaloisActionIsAdicContinuous A self.ρ

def GaloisRepAdic.IsUnramifiedAt {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) (q : ℕ) : Prop

Inertia acts trivially at every valuation above the specified rational prime.

Equations

• ρ.IsUnramifiedAt q = ∀ (P : ValuationSubring (AlgebraicClosure ℚ)), P.LiesOverPrime q → ∀ σ ∈ ValuationSubring.inertiaSubgroupIn ℚ P, ρ.ρ σ = 1

noncomputable def GaloisRepAdic.det {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) : Gal(AlgebraicClosure ℚ/ℚ) →* Aˣ

The determinant character of the Galois representation, valued in units of the coefficient ring.

Equations

• ρ.det = (LinearMap.det.comp ρ.ρ).toHomUnits

noncomputable def GaloisRepAdic.trace {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) (σ : Gal(AlgebraicClosure ℚ/ℚ)) : A

The trace of a Galois element acting on the coefficient module.

Equations

• ρ.trace σ = (LinearMap.trace A ρ.V) (ρ.ρ σ)

noncomputable def GaloisRepAdic.baseChangeAlong {A : Type} [CommRing A] [IsLocalRing A] {B : Type} [CommRing B] [IsLocalRing B] (φ : A →+* B) (hφ : IsLocalHom φ) (ρ : GaloisRepAdic A) : GaloisRepAdic B

Extend the representation's coefficients along a local ring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaloisRepAdic.residual {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) : ResidualGaloisRep (IsLocalRing.ResidueField A)

Reduce the representation to the residue field of its coefficient ring.

Equations

• One or more equations did not get rendered due to their size.

structure GaloisRepAdic.Equiv {A : Type} [CommRing A] [IsLocalRing A] (ρ₁ ρ₂ : GaloisRepAdic A) : Type

A linear equivalence intertwining two adic Galois representations.

• toLinearEquiv : ρ₁.V ≃ₗ[A] ρ₂.V

  The underlying linear equivalence between the coefficient modules.

• map_apply (σ : Gal(AlgebraicClosure ℚ/ℚ)) (x : ρ₁.V) : self.toLinearEquiv ((ρ₁.ρ σ) x) = (ρ₂.ρ σ) (self.toLinearEquiv x)

def GaloisRepAdic.IsEquiv {A : Type} [CommRing A] [IsLocalRing A] (ρ₁ ρ₂ : GaloisRepAdic A) : Prop

There exists a linear equivalence intertwining the two Galois actions.

Equations

• ρ₁.IsEquiv ρ₂ = Nonempty (ρ₁.Equiv ρ₂)

def GaloisRepAdic.Equiv.refl {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) : ρ.Equiv ρ

The identity intertwining equivalence of an adic Galois representation.

Equations

• GaloisRepAdic.Equiv.refl ρ = { toLinearEquiv := LinearEquiv.refl A ρ.V, map_apply := ⋯ }

def GaloisRepAdic.Equiv.symm {A : Type} [CommRing A] [IsLocalRing A] {ρ₁ ρ₂ : GaloisRepAdic A} (e : ρ₁.Equiv ρ₂) : ρ₂.Equiv ρ₁

The inverse of an intertwining equivalence.

Equations

• e.symm = { toLinearEquiv := e.toLinearEquiv.symm, map_apply := ⋯ }

def GaloisRepAdic.Equiv.trans {A : Type} [CommRing A] [IsLocalRing A] {ρ₁ ρ₂ ρ₃ : GaloisRepAdic A} (e : ρ₁.Equiv ρ₂) (e' : ρ₂.Equiv ρ₃) : ρ₁.Equiv ρ₃

The composite of two intertwining equivalences.

Equations

• e.trans e' = { toLinearEquiv := e.toLinearEquiv.trans e'.toLinearEquiv, map_apply := ⋯ }

noncomputable def GaloisRepAdic.Equiv.baseChangeAlong {A : Type} [CommRing A] [IsLocalRing A] {B : Type} [CommRing B] [IsLocalRing B] (φ : A →+* B) (hφ : IsLocalHom φ) {ρ₁ ρ₂ : GaloisRepAdic A} (e : ρ₁.Equiv ρ₂) : (GaloisRepAdic.baseChangeAlong φ hφ ρ₁).Equiv (GaloisRepAdic.baseChangeAlong φ hφ ρ₂)

Extend an intertwining equivalence along a local homomorphism of coefficient rings.

Equations

• GaloisRepAdic.Equiv.baseChangeAlong φ hφ e = { toLinearEquiv := LinearEquiv.baseChange A B ρ₁.V ρ₂.V e.toLinearEquiv, map_apply := ⋯ }

noncomputable def GaloisRepAdic.Equiv.residual {A : Type} [CommRing A] [IsLocalRing A] {ρ₁ ρ₂ : GaloisRepAdic A} (e : ρ₁.Equiv ρ₂) : ρ₁.residual.Equiv ρ₂.residual

The intertwining equivalence obtained by reducing coefficients to the residue field.

Equations

• e.residual = { toLinearEquiv := LinearEquiv.baseChange A (IsLocalRing.ResidueField A) ρ₁.V ρ₂.V e.toLinearEquiv, map_apply := ⋯ }

def GaloisRepAdic.toResidualGaloisRep {k : Type} [Field k] (ρ : GaloisRepAdic k) : ResidualGaloisRep k

View an adic representation over a field as a residual representation over the same field.

Equations

• ρ.toResidualGaloisRep = { V := ρ.V, instAddCommGroup := ρ.instAddCommGroup, instModule := ρ.instModule, finrank_eq := ⋯, ρ := ρ.ρ, factorsThroughFiniteLevel := ⋯ }

def GaloisRepAdic.ofResidualGaloisRep {k : Type} [Field k] (ρ : ResidualGaloisRep k) : GaloisRepAdic k

View a residual representation as an adic representation over its coefficient field.

Equations

• One or more equations did not get rendered due to their size.