The p-adic Tate module and the Tate module Galois representation #

Definition: EllipticCurve_TateModule (e3517e0d-3db6-5cee-a949-fb0cba7e3bee), by Claude, 2026-09-05.

For a natural number $p$ and an additive commutative group $M$, TateModule p M is defined as the additive subgroup of sequences $x : \mathbb{N} \to M$ satisfying, for every $n$, the two conditions $p^n \cdot x_n = 0$ and $p \cdot x_{n+1} = x_n$; thus it is the inverse limit $\varprojlim M[p^n]$ realised concretely as sequences (the condition at $n = 0$ forces $x_0 = 0$, so the zeroth term is always trivial). For $p$ prime it is given a $\mathbb{Z}_p$-module structure in which $a \in \mathbb{Z}_p$ acts at level $n$ through the integer a.appr n representing $a$ modulo $p^n$; smul_apply_eq_smul checks that when $M$ is already a $\mathbb{Z}_p$-module this agrees with the pointwise action. Further contents: the level maps proj p M n : TateModule p M →+ M, landing in Submodule.torsionBy ℤ M ((p^n : ℕ) : ℤ), with proj_eq_zero_iff identifying the kernel of proj … n with $\mathfrak{m}^n \cdot \top$ for $\mathfrak{m}$ the maximal ideal of $\mathbb{Z}_p$; and rep p M G : G →* Module.End ℤ_[p] (TateModule p M), the $\mathbb{Z}_p$-linear action induced termwise by any distributive action of a monoid $G$ on $M$.

A later section takes as an explicit hypothesis the counting assumption that for every $n$ the subgroup Submodule.torsionBy ℤ M ((p^n : ℕ) : ℤ) has exactly $(p^n)^2$ elements, and deduces from it that multiplication by $p$ sends $M[p^{n+1}]$ onto $M[p^n]$, hence that each proj … n is surjective onto $M[p^n]$, and constructs from this an explicit basis indexed by Fin 2; free, finite and finrank_eq_two follow.

For a Weierstrass curve $W$ over $\mathbb{Q}$, torsionField W p n is the subfield of $\overline{\mathbb{Q}}$ generated by the affine coordinates of the $p^n$-torsion $\overline{\mathbb{Q}}$-points; it is shown finite-dimensional when that torsion group is finite, and it witnesses the project's adic-continuity condition GaloisActionIsAdicContinuous for rep. Under the same counting assumption, tateModuleRepOfBasis and tateModuleRep package the Tate module of the $\overline{\mathbb{Q}}$-points, with the coordinatewise $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$-action, as a GaloisRepAdic ℤ_[p]. Independently, GaloisRep.padicIntToRing 𝒪 p hp is the ring homomorphism $\mathbb{Z}_p \to \mathcal{O}$ obtained, for a local ring $\mathcal{O}$ that is adically complete for its maximal ideal and has $p \in \mathfrak{m}_\mathcal{O}$, by lifting the compatible maps $\mathbb{Z}_p \to \mathbb{Z}/p^n \to \mathcal{O}/\mathfrak{m}^n$; it is characterised by that compatibility, is a local homomorphism, and is the identity for $\mathcal{O} = \mathbb{Z}_p$.

Relation to Mathlib. Mathlib has no $p$-adic Tate module; the subgroup of $\mathbb{N}$-indexed compatible torsion sequences, its $\mathbb{Z}_p$-action via PadicInt.appr, and the induced representation rep are the project's own, built on Mathlib's PadicInt, Submodule.torsionBy and WeierstrassCurve. GaloisRep.padicIntToRing is assembled from Mathlib's IsAdicComplete.liftRingHom. The freeness and rank-two results are stated relative to the explicit counting assumption on the orders of the torsion subgroups, which is not deduced from ellipticity here but must be supplied by the consumer.

Where it is used. The representation WeierstrassCurve.tateModuleRep is the Galois-side input to modularity lifting for the Frey curve: it supplies the two-dimensional $p$-adic representation whose residual representation is compared with the mod $p$ representation on $W[p]$, and whose ramification behaviour is the subject of separate statements. GaloisRep.padicIntToRing is used to move its coefficients from $\mathbb{Z}_p$ to a general complete local coefficient ring.