definition · Pro-C groups

The full Tate module of an abelian group

Compatible torsion points at every positive integer form a torsion-free inverse-limit object.

Coherence across levels explains torsion-freeness: a family killed by a positive integer n has each coordinate equal to n times a higher coordinate, hence zero. Using all positive integers retains every prime-power direction. Tate’s 1967 paper on p-divisible groups treats the prime-power setting; here the same inverse-limit idea applies to arbitrary abelian groups without choosing a single prime.

ProCGroups on GitHub ↗

Mathematical statement

For an abelian group $M$, put $M[n]=\{x\in M:nx=0\}$. The full Tate module is $$T(M)=\{(x_n)_{n\ge1}:x_n\in M[n],\;m x_{nm}=x_n\text{ for }n,m\ge1\}.$$ The transition from level $nm$ to level $n$ is multiplication by $m$.

The definition applies to an arbitrary abelian group. The source also proves that if $n>0$ and $n x=0$ for $x\in T(M)$, then $x=0$. Thus this compatible-family group is torsion-free.

Lean code

`ProCGroups.FullTateModule`

Published library source ↗Same source in NYLL ↗

def FullTateModule : Type u

In-scope Lean context

namespace ProCGroups

universe u

variable (M : Type u) [AddCommGroup M]

Full declaration and proof

/-- The full Tate module, realized as compatible actual torsion families. -/
def FullTateModule : Type u := ↥(compatibleTorsionFamilies M)

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

J. T. Tate. p-Divisible Groups. Springer, Berlin, Heidelberg, 158–183, 1967. In Proceedings of a Conference on Local Fields.

Published source: 7d74e3a9.

← All selected results in Pro-C groups