The Tate module of an elliptic curve

The torsion levels of an elliptic curve are finite. Consequently the inverse-limit topology on its Tate module is compact, Hausdorff, and totally disconnected. Hausdorffness and total disconnectedness hold for every TauCeti.TateModule; this file supplies the elliptic-curve input needed for compactness.

Over a separably closed field in which the prime ℓ is invertible, the level E[ℓ ^ n] has (ℓ ^ n) ^ 2 elements, so the Tate module T_ℓ E is a free ℤ_ℓ-module of rank 2 (Silverman III.7.1). This is the module on which the ℓ-adic Galois representation and the ℓ-adic Weil pairing of an elliptic curve live.

Main results

• WeierstrassCurve.natCard_tateModuleLevel: E[ℓ ^ n] has (ℓ ^ n) ^ 2 elements.
• WeierstrassCurve.nonempty_linearEquiv_tateModule: T_ℓ E ≃ ℤ_ℓ².
• WeierstrassCurve.free_tateModule, WeierstrassCurve.finite_tateModule, WeierstrassCurve.finrank_tateModule: T_ℓ E is free and finitely generated of rank 2.

References

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

instance WeierstrassCurve.instCompactSpaceTateModule {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (p : ℕ) [NeZero p] : CompactSpace (TauCeti.TateModule p W.toAffine.Point)

The Tate module of an elliptic curve at a nonzero natural number is compact. It is a closed subgroup of the product of the finite torsion groups E[p^n].

theorem WeierstrassCurve.natCard_tateModuleLevel {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {ℓ : ℕ} (hℓ : ↑ℓ ≠ 0) (n : ℕ) : Nat.card (TauCeti.TateModuleLevel ℓ W.toAffine.Point n) = (ℓ ^ n) ^ 2

Over a separably closed field in which ℓ is invertible, the ℓ ^ n-torsion of an elliptic curve has (ℓ ^ n) ^ 2 elements.

theorem WeierstrassCurve.nonempty_linearEquiv_tateModule {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) : Nonempty (TauCeti.TateModule ℓ W.toAffine.Point ≃ₗ[ℤ_[ℓ]] Fin 2 → ℤ_[ℓ])

The Tate module T_ℓ E is free of rank 2 over ℤ_ℓ, over a separably closed field in which the prime ℓ is invertible. The isomorphism is noncanonical, so the result asserts its existence.

theorem WeierstrassCurve.free_tateModule {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) : Module.Free ℤ_[ℓ] (TauCeti.TateModule ℓ W.toAffine.Point)

The Tate module T_ℓ E is a free ℤ_ℓ-module, over a separably closed field in which the prime ℓ is invertible.

theorem WeierstrassCurve.finite_tateModule {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) : Module.Finite ℤ_[ℓ] (TauCeti.TateModule ℓ W.toAffine.Point)

The Tate module T_ℓ E is a finitely generated ℤ_ℓ-module, over a separably closed field in which the prime ℓ is invertible.

theorem WeierstrassCurve.finrank_tateModule {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) : Module.finrank ℤ_[ℓ] (TauCeti.TateModule ℓ W.toAffine.Point) = 2

The Tate module T_ℓ E has rank 2 over ℤ_ℓ, over a separably closed field in which the prime ℓ is invertible.