Tate modules of abelian groups

For an abelian group A and a prime p, its p-adic Tate module is the inverse limit

TateModule p A = lim_n A[p^n]

along the transition maps A[p^(n+1)] → A[p^n], x ↦ p • x. This file gives the inverse limit a concrete carrier, its universal property, the inverse-limit topology, and its canonical ℤ_p-module structure. The action at level n is through reduction ℤ_p → ZMod (p ^ n).

The construction applies in particular to the point group of an elliptic curve. Finite-level torsion calculations can therefore be assembled into the ℓ-adic representation without introducing an elliptic-curve-specific copy of the inverse-limit machinery.

Main definitions

• TauCeti.tateModuleSubgroup: the subgroup of compatible p-power torsion families.
• TauCeti.TateModule: the p-adic Tate module, with its ℤ_p-module and inverse-limit topology.
• TauCeti.TateModule.proj: projection to A[p^n].
• TauCeti.TateModule.lift: the map into the Tate module induced by compatible finite-level maps.
• TauCeti.TateModule.mapLinearMap: the ℤ_p-linear map induced by an additive homomorphism.

Main results

• TauCeti.TateModule.proj_succ: consecutive components satisfy p • x_(n+1) = x_n.
• TauCeti.TateModule.proj_smul: projection is semilinear for reduction ℤ_p → ZMod (p ^ n).
• TauCeti.TateModule.continuous_iff: a map into the Tate module is continuous exactly when all its finite-level components are locally constant.
• TauCeti.TateModule.continuous_map_apply: a family of homomorphisms moving each torsion point locally constantly acts jointly continuously on Tate modules.
• TauCeti.TateModule.surjective_of_forall_surjective_proj: a continuous map from a compact space into the Tate module is surjective when each of its components is.
• TauCeti.TateModule.proj_surjective: if the transition maps are surjective, so is every projection.
• TauCeti.TateModule.nonempty_linearEquiv_of_natCard: if A[p^n] has (p^n)^r elements for every n, then T_p A ≃ ℤ_p^r; hence T_p A is free of rank r (TauCeti.TateModule.free_of_natCard, TauCeti.TateModule.finrank_eq_of_natCard).

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.7.

@[reducible, inline]

abbrev TauCeti.TateModuleLevel (p : ℕ) (A : Type u_1) [AddCommGroup A] (n : ℕ) : Type u_1

The n-th level A[p^n] of the p-power torsion tower.

Equations

• TauCeti.TateModuleLevel p A n = ↥(AddSubgroup.torsionBy A ↑(p ^ n))

def TauCeti.tateModuleTransition (p : ℕ) (A : Type u_1) [AddCommGroup A] (n : ℕ) : TateModuleLevel p A (n + 1) →+ TateModuleLevel p A n

The transition map A[p^(n+1)] → A[p^n], given by multiplication by p.

Equations

• TauCeti.tateModuleTransition p A n = { toFun := fun (x : TauCeti.TateModuleLevel p A (n + 1)) => ⟨p • ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.tateModuleTransition_apply (p : ℕ) (A : Type u_1) [AddCommGroup A] (n : ℕ) (x : TateModuleLevel p A (n + 1)) : ↑((tateModuleTransition p A n) x) = p • ↑x

The transition map is multiplication by p on the underlying group.

def TauCeti.tateModuleSubgroup (p : ℕ) (A : Type u_1) [AddCommGroup A] : AddSubgroup ((n : ℕ) → TateModuleLevel p A n)

The subgroup of the product of the groups A[p^n] consisting of families compatible under multiplication by p. Its carrier is TateModule p A.

Equations

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

theorem TauCeti.mem_tateModuleSubgroup_iff {p : ℕ} {A : Type u_1} [AddCommGroup A] {x : (n : ℕ) → TateModuleLevel p A n} : x ∈ tateModuleSubgroup p A ↔ ∀ (n : ℕ), (tateModuleTransition p A n) (x (n + 1)) = x n

A family of p-power torsion points lies in the Tate module exactly when consecutive components are compatible under multiplication by p.

def TauCeti.TateModule (p : ℕ) (A : Type u_1) [AddCommGroup A] : Type u_1

The p-adic Tate module of an abelian group: compatible families of p^n-torsion points.

Equations

• TauCeti.TateModule p A = ↥(TauCeti.tateModuleSubgroup p A)

@[instance_reducible]

noncomputable instance TauCeti.TateModule.instAddCommGroup (p : ℕ) (A : Type u_1) [AddCommGroup A] : AddCommGroup (TateModule p A)

Equations

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

noncomputable def TauCeti.TateModule.proj {p : ℕ} {A : Type u_1} [AddCommGroup A] (n : ℕ) : TateModule p A →+ TateModuleLevel p A n

Projection of the Tate module to its p^n-torsion level.

Equations

• TauCeti.TateModule.proj n = (Pi.evalAddMonoidHom (fun (n : ℕ) => TauCeti.TateModuleLevel p A n) n).comp (TauCeti.tateModuleSubgroup p A).subtype

@[simp]

theorem TauCeti.TateModule.proj_succ {p : ℕ} {A : Type u_1} [AddCommGroup A] (x : TateModule p A) (n : ℕ) : (tateModuleTransition p A n) ((proj (n + 1)) x) = (proj n) x

Consecutive components of a Tate-module point are compatible under multiplication by p.

theorem TauCeti.TateModule.ext {p : ℕ} {A : Type u_1} [AddCommGroup A] {x y : TateModule p A} (h : ∀ (n : ℕ), (proj n) x = (proj n) y) : x = y

A Tate-module point is determined by all of its finite-level components.

theorem TauCeti.TateModule.ext_iff {p : ℕ} {A : Type u_1} [AddCommGroup A] {x y : TateModule p A} : x = y ↔ ∀ (n : ℕ), (proj n) x = (proj n) y

noncomputable def TauCeti.TateModule.mk {p : ℕ} {A : Type u_1} [AddCommGroup A] (x : (n : ℕ) → TateModuleLevel p A n) (hx : ∀ (n : ℕ), (tateModuleTransition p A n) (x (n + 1)) = x n) : TateModule p A

The Tate-module point with prescribed compatible components.

Equations

• TauCeti.TateModule.mk x hx = ⟨x, hx⟩

@[simp]

theorem TauCeti.TateModule.proj_mk {p : ℕ} {A : Type u_1} [AddCommGroup A] (x : (n : ℕ) → TateModuleLevel p A n) (hx : ∀ (n : ℕ), (tateModuleTransition p A n) (x (n + 1)) = x n) (n : ℕ) : (proj n) (mk x hx) = x n

The projection of a point constructed by mk is its prescribed component.

theorem TauCeti.TateModule.range_proj {p : ℕ} {A : Type u_1} [AddCommGroup A] : (Set.range fun (x : TateModule p A) (n : ℕ) => (proj n) x) = ↑(tateModuleSubgroup p A)

The family of projections identifies the Tate module with the subgroup of compatible families in the product of the torsion levels.

noncomputable def TauCeti.TateModule.lift {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddZeroClass B] (f : (n : ℕ) → B →+ TateModuleLevel p A n) (hf : ∀ (n : ℕ), (tateModuleTransition p A n).comp (f (n + 1)) = f n) : B →+ TateModule p A

The additive homomorphism into a Tate module determined by compatible finite-level maps.

Equations

• TauCeti.TateModule.lift f hf = (AddMonoidHom.pi f).codRestrict (TauCeti.tateModuleSubgroup p A) ⋯

@[simp]

theorem TauCeti.TateModule.proj_lift {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddZeroClass B] (f : (n : ℕ) → B →+ TateModuleLevel p A n) (hf : ∀ (n : ℕ), (tateModuleTransition p A n).comp (f (n + 1)) = f n) (n : ℕ) : (proj n).comp (lift f hf) = f n

Projection after lift recovers the corresponding finite-level homomorphism.

theorem TauCeti.TateModule.lift_unique {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddZeroClass B] (f : (n : ℕ) → B →+ TateModuleLevel p A n) (hf : ∀ (n : ℕ), (tateModuleTransition p A n).comp (f (n + 1)) = f n) (g : B →+ TateModule p A) (hg : ∀ (n : ℕ), (proj n).comp g = f n) : g = lift f hf

The lift of a compatible family of finite-level maps is unique.

def TauCeti.TateModule.levelMap {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] (f : A →+ B) (n : ℕ) : TateModuleLevel p A n →+ TateModuleLevel p B n

The map on the p^n-torsion levels induced by an additive homomorphism.

Equations

• TauCeti.TateModule.levelMap f n = (f.comp (AddSubgroup.torsionBy A ↑(p ^ n)).subtype).codRestrict (AddSubgroup.torsionBy B ↑(p ^ n)) ⋯

@[simp]

theorem TauCeti.TateModule.levelMap_apply {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] (f : A →+ B) (n : ℕ) (x : TateModuleLevel p A n) : ↑((levelMap f n) x) = f ↑x

The map induced on a torsion level agrees with the original homomorphism on underlying elements.

noncomputable def TauCeti.TateModule.map {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] (f : A →+ B) : TateModule p A →+ TateModule p B

An additive homomorphism induces an additive homomorphism of Tate modules, componentwise.

Equations

• TauCeti.TateModule.map f = (AddMonoidHom.pi fun (n : ℕ) => (TauCeti.TateModule.levelMap f n).comp (TauCeti.TateModule.proj n)).codRestrict (TauCeti.tateModuleSubgroup p B) ⋯

@[simp]

theorem TauCeti.TateModule.proj_map {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] (f : A →+ B) (x : TateModule p A) (n : ℕ) : (proj n) ((map f) x) = (levelMap f n) ((proj n) x)

The map induced on Tate modules is computed componentwise.

@[simp]

theorem TauCeti.TateModule.map_id {p : ℕ} {A : Type u_1} [AddCommGroup A] : map (AddMonoidHom.id A) = AddMonoidHom.id (TateModule p A)

Tate modules send identity homomorphisms to identity homomorphisms.

@[simp]

theorem TauCeti.TateModule.map_comp {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] {C : Type u_3} [AddCommGroup C] (g : B →+ C) (f : A →+ B) : map (g.comp f) = (map g).comp (map f)

Tate modules send compositions to compositions.

@[instance_reducible]

instance TauCeti.TateModule.levelZModModule {p : ℕ} {A : Type u_1} [AddCommGroup A] (n : ℕ) : Module (ZMod (p ^ n)) (TateModuleLevel p A n)

The canonical module structure on the p^n-torsion level over ZMod (p^n).

Equations

• TauCeti.TateModule.levelZModModule n = AddSubgroup.torsionBy.zmodModule

@[instance_reducible]

noncomputable instance TauCeti.TateModule.instSMulPadicInt {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] : SMul ℤ_[p] (TateModule p A)

Scalar multiplication by ℤ_p, obtained by reducing a scalar modulo p^n on the n-th torsion level.

Equations

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

@[simp]

theorem TauCeti.TateModule.proj_smul {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] (a : ℤ_[p]) (x : TateModule p A) (n : ℕ) : (proj n) (a • x) = (PadicInt.toZModPow n) a • (proj n) x

Scalar multiplication on the n-th projection is reduction modulo p^n.

@[instance_reducible]

noncomputable instance TauCeti.TateModule.instModulePadicInt {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] : Module ℤ_[p] (TateModule p A)

The Tate module is canonically a module over the p-adic integers.

Equations

• TauCeti.TateModule.instModulePadicInt = { toSMul := TauCeti.TateModule.instSMulPadicInt, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def TauCeti.TateModule.mapLinearMap {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] {B : Type u_2} [AddCommGroup B] (f : A →+ B) : TateModule p A →ₗ[ℤ_[p]] TateModule p B

An additive homomorphism induces a ℤ_p-linear map on Tate modules.

Equations

• TauCeti.TateModule.mapLinearMap f = { toAddHom := ↑(TauCeti.TateModule.map f), map_smul' := ⋯ }

@[simp]

theorem TauCeti.TateModule.mapLinearMap_apply {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] {B : Type u_2} [AddCommGroup B] (f : A →+ B) (x : TateModule p A) : (mapLinearMap f) x = (map f) x

The linear map induced on Tate modules has the same underlying additive map as map.

The inverse-limit topology

@[instance_reducible]

noncomputable instance TauCeti.TateModule.instTopologicalSpace {p : ℕ} {A : Type u_1} [AddCommGroup A] : TopologicalSpace (TateModule p A)

The inverse-limit topology, induced from the product of the discrete torsion levels.

Equations

• TauCeti.TateModule.instTopologicalSpace = TopologicalSpace.induced (fun (x : TauCeti.TateModule p A) (n : ℕ) => (TauCeti.TateModule.proj n) x) Pi.topologicalSpace

theorem TauCeti.TateModule.continuous_iff {p : ℕ} {A : Type u_1} [AddCommGroup A] {X : Type u_2} [TopologicalSpace X] {f : X → TateModule p A} : Continuous f ↔ ∀ (n : ℕ), IsLocallyConstant fun (x : X) => (proj n) (f x)

A map into a Tate module is continuous exactly when all its finite-level components are locally constant.

theorem TauCeti.TateModule.isLocallyConstant_proj {p : ℕ} {A : Type u_1} [AddCommGroup A] (n : ℕ) : IsLocallyConstant ⇑(proj n)

Every finite-level projection is locally constant.

instance TauCeti.TateModule.instIsTopologicalAddGroup {p : ℕ} {A : Type u_1} [AddCommGroup A] : IsTopologicalAddGroup (TateModule p A)

instance TauCeti.TateModule.instContinuousSMulPadicInt {p : ℕ} {A : Type u_1} [AddCommGroup A] [Fact (Nat.Prime p)] : ContinuousSMul ℤ_[p] (TateModule p A)

The canonical action of the p-adic integers on the Tate module is jointly continuous.

instance TauCeti.TateModule.instT2Space {p : ℕ} {A : Type u_1} [AddCommGroup A] : T2Space (TateModule p A)

instance TauCeti.TateModule.instTotallyDisconnectedSpace {p : ℕ} {A : Type u_1} [AddCommGroup A] : TotallyDisconnectedSpace (TateModule p A)

instance TauCeti.TateModule.instCompactSpaceOfFiniteTateModuleLevel {p : ℕ} {A : Type u_1} [AddCommGroup A] [∀ (n : ℕ), Finite (TateModuleLevel p A n)] : CompactSpace (TateModule p A)

If all p-power torsion levels are finite, then the Tate module is compact.

theorem TauCeti.TateModule.continuous_map {p : ℕ} {A : Type u_1} [AddCommGroup A] {B : Type u_2} [AddCommGroup B] (f : A →+ B) : Continuous ⇑(map f)

The homomorphism on Tate modules induced by an additive homomorphism is continuous.

theorem TauCeti.TateModule.continuous_map_apply {p : ℕ} {A : Type u_1} [AddCommGroup A] {G : Type u_2} [TopologicalSpace G] {B : Type u_3} [AddCommGroup B] {f : G → A →+ B} (hf : ∀ (n : ℕ) (x : TateModuleLevel p A n), IsLocallyConstant fun (g : G) => (f g) ↑x) : Continuous fun (q : G × TateModule p A) => (map (f q.1)) q.2

Homomorphisms moving torsion locally constantly act continuously on Tate modules. If f : G → (A →+ B) is a family of homomorphisms parametrised by a topological space G, and g ↦ f g x is locally constant for every p-power torsion point x, then (g, y) ↦ map (f g) y is jointly continuous. This is how a profinite Galois group acting on the torsion points of A acts continuously on T_p A.

Freeness

theorem TauCeti.TateModule.coe_proj_eq_pow_nsmul {p : ℕ} {A : Type u_1} [AddCommGroup A] (x : TateModule p A) (m k : ℕ) : ↑((proj m) x) = p ^ k • ↑((proj (m + k)) x)

The components of a Tate-module point satisfy x_m = p ^ k • x_(m + k).

theorem TauCeti.TateModule.coe_proj_eq_pow_sub_nsmul {p : ℕ} {A : Type u_1} [AddCommGroup A] (x : TateModule p A) {m n : ℕ} (h : m ≤ n) : ↑((proj m) x) = p ^ (n - m) • ↑((proj n) x)

The components of a Tate-module point satisfy x_m = p ^ (n - m) • x_n for m ≤ n.

theorem TauCeti.TateModule.surjective_of_forall_surjective_proj {p : ℕ} {A : Type u_1} [AddCommGroup A] {X : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : X → TateModule p A} (hf : Continuous f) (h : ∀ (n : ℕ), Function.Surjective fun (x : X) => (proj n) (f x)) : Function.Surjective f

Surjectivity from the finite levels. A continuous map from a compact space into a Tate module is surjective as soon as each of its components is surjective.

theorem TauCeti.TateModule.proj_surjective {p : ℕ} {A : Type u_1} [AddCommGroup A] (h : ∀ (n : ℕ), Function.Surjective ⇑(tateModuleTransition p A n)) (n : ℕ) : Function.Surjective ⇑(proj n)

If every transition map is surjective, then every point of every torsion level is a component of a Tate-module point.

theorem TauCeti.TateModule.tateModuleTransition_surjective_of_natCard {p : ℕ} {A : Type u_1} [AddCommGroup A] {r : ℕ} (hp : p ≠ 0) (hcard : ∀ (n : ℕ), Nat.card (TateModuleLevel p A n) = (p ^ n) ^ r) (n : ℕ) : Function.Surjective ⇑(tateModuleTransition p A n)

If the p ^ n-torsion has (p ^ n) ^ r elements for every n, then multiplication by p maps A[p ^ (n + 1)] onto A[p ^ n].

theorem TauCeti.TateModule.coe_zmod_smul {p : ℕ} {A : Type u_1} [AddCommGroup A] [NeZero p] {n : ℕ} (z : ZMod (p ^ n)) (y : TateModuleLevel p A n) : ↑(z • y) = z.val • ↑y

The ZMod (p ^ n)-action on the n-th torsion level is multiplication by a representative.

theorem TauCeti.TateModule.nonempty_linearEquiv_of_natCard {p : ℕ} {A : Type u_1} [AddCommGroup A] [hp : Fact (Nat.Prime p)] {r : ℕ} (hcard : ∀ (n : ℕ), Nat.card (TateModuleLevel p A n) = (p ^ n) ^ r) : Nonempty (TateModule p A ≃ₗ[ℤ_[p]] Fin r → ℤ_[p])

A Tate module whose p ^ n-torsion levels have (p ^ n) ^ r elements is free of rank r: it is isomorphic to ℤ_p ^ r. The isomorphism is noncanonical, so the result asserts its existence.

theorem TauCeti.TateModule.free_of_natCard {p : ℕ} {A : Type u_1} [AddCommGroup A] [hp : Fact (Nat.Prime p)] {r : ℕ} (hcard : ∀ (n : ℕ), Nat.card (TateModuleLevel p A n) = (p ^ n) ^ r) : Module.Free ℤ_[p] (TateModule p A)

A Tate module whose p ^ n-torsion levels have (p ^ n) ^ r elements is free over ℤ_p.

theorem TauCeti.TateModule.finite_of_natCard {p : ℕ} {A : Type u_1} [AddCommGroup A] [hp : Fact (Nat.Prime p)] {r : ℕ} (hcard : ∀ (n : ℕ), Nat.card (TateModuleLevel p A n) = (p ^ n) ^ r) : Module.Finite ℤ_[p] (TateModule p A)

A Tate module whose p ^ n-torsion levels have (p ^ n) ^ r elements is finitely generated over ℤ_p.

theorem TauCeti.TateModule.finrank_eq_of_natCard {p : ℕ} {A : Type u_1} [AddCommGroup A] [hp : Fact (Nat.Prime p)] {r : ℕ} (hcard : ∀ (n : ℕ), Nat.card (TateModuleLevel p A n) = (p ^ n) ^ r) : Module.finrank ℤ_[p] (TateModule p A) = r

A Tate module whose p ^ n-torsion levels have (p ^ n) ^ r elements has rank r over ℤ_p.