The p-adic Tate twist

The p-adic Tate twist ℤ_p(1) over a commutative monoid K is the inverse limit of its groups of p ^ n-th roots of unity along the p-th power maps. Written additively, this is the Tate module of the unit group:

PadicTateTwist p K = TateModule p (Additive Kˣ).

This file identifies the finite levels with Additive (rootsOfUnity (p ^ n) K). When K has enough p-power roots of unity (for example, a separably closed field in which p is nonzero), the twist is a free ℤ_p-module of rank one. Ring automorphisms act on it componentwise; when all p-power roots of unity exist, this action is scalar multiplication by Mathlib's p-adic cyclotomic character. These are the coefficient module and action used by p-adic Weil pairings.

For ℓ nonzero and prime to p, the powers ℓ ^ n are levels of the prime-to-p Tate module ℤ̂^{(p')}(1) = lim_{p ∤ m} μ_m, and keeping the components at these levels is a continuous, Galois-equivariant homomorphism ℤ̂^{(p')}(1) → ℤ_ℓ(1).

Main definitions

• TauCeti.PadicTateTwist: the inverse limit ℤ_p(1).
• TauCeti.PadicTateTwist.proj: projection to μ_{p^n}, in additive notation.
• TauCeti.PadicTateTwist.galoisRepresentation: the componentwise action of field automorphisms.
• TauCeti.PrimeToPTateModule.toPadicTateTwist: the ℓ-adic component ℤ̂^{(p')}(1) → ℤ_ℓ(1) of the prime-to-p Tate module, for ℓ prime to p.

Main results

• TauCeti.PadicTateTwist.levelAddEquivRootsOfUnity: the n-th level is μ_{p^n}.
• TauCeti.PadicTateTwist.instCompactSpace: for nonzero p, ℤ_p(1) is compact over a domain.
• TauCeti.PadicTateTwist.nonempty_linearEquiv: when K has enough p-power roots of unity, ℤ_p(1) is noncanonically linearly equivalent to ℤ_p.
• TauCeti.PadicTateTwist.galoisRepresentation_apply_eq_smul: the Galois action is scalar multiplication by the cyclotomic character.
• TauCeti.PadicTateTwist.continuous_galoisRepresentation: this action is jointly continuous.
• TauCeti.PrimeToPTateModule.proj_toPadicTateTwist: the components of the ℓ-adic component are the components of level ℓ ^ n.
• TauCeti.PrimeToPTateModule.toPadicTateTwist_smul: the ℓ-adic component is Galois-equivariant.

References

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

@[reducible, inline]

abbrev TauCeti.PadicTateTwist (p : ℕ) (K : Type u_1) [CommMonoid K] : Type u_1

The p-adic Tate twist ℤ_p(1), realised as the Tate module of the multiplicative group. Its n-th component is the group μ_{p^n} of p ^ n-th roots of unity.

Equations

• TauCeti.PadicTateTwist p K = TauCeti.TateModule p (Additive Kˣ)

def TauCeti.PadicTateTwist.levelAddEquivRootsOfUnity {p : ℕ} {K : Type u_1} [CommMonoid K] (n : ℕ) : TateModuleLevel p (Additive Kˣ) n ≃+ Additive ↥(rootsOfUnity (p ^ n) K)

The p ^ n-torsion in the additive unit group is the group of p ^ n-th roots of unity, written additively.

Equations

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

@[simp]

theorem TauCeti.PadicTateTwist.coe_levelAddEquivRootsOfUnity_symm {p : ℕ} {K : Type u_1} [CommMonoid K] (n : ℕ) (ζ : Additive ↥(rootsOfUnity (p ^ n) K)) : ↑((levelAddEquivRootsOfUnity n).symm ζ) = Additive.ofMul ↑(Additive.toMul ζ)

The inverse finite-level equivalence forgets the roots-of-unity membership proof.

noncomputable def TauCeti.PadicTateTwist.proj {p : ℕ} {K : Type u_1} [CommMonoid K] (n : ℕ) : PadicTateTwist p K →+ Additive ↥(rootsOfUnity (p ^ n) K)

Projection of ℤ_p(1) to its p ^ n-th roots-of-unity level.

Equations

• TauCeti.PadicTateTwist.proj n = (TauCeti.PadicTateTwist.levelAddEquivRootsOfUnity n).toAddMonoidHom.comp (TauCeti.TateModule.proj n)

theorem TauCeti.PadicTateTwist.proj_def {p : ℕ} {K : Type u_1} [CommMonoid K] (n : ℕ) (x : PadicTateTwist p K) : (proj n) x = (levelAddEquivRootsOfUnity n) ((TateModule.proj n) x)

The roots-of-unity projection is the finite-level equivalence after ordinary projection.

@[simp]

theorem TauCeti.PadicTateTwist.coe_proj {p : ℕ} {K : Type u_1} [CommMonoid K] (x : PadicTateTwist p K) (n : ℕ) : ↑(Additive.toMul ((proj n) x)) = Additive.toMul ↑((TateModule.proj n) x)

The roots-of-unity projection is the ordinary Tate-module projection on underlying units.

@[simp]

theorem TauCeti.PadicTateTwist.coe_tateModuleProj_succ_pow {p : ℕ} {K : Type u_1} [CommMonoid K] (x : PadicTateTwist p K) (n : ℕ) : Additive.toMul ↑((TateModule.proj (n + 1)) x) ^ p = Additive.toMul ↑((TateModule.proj n) x)

Consecutive components of ℤ_p(1) are related by the p-th power map.

theorem TauCeti.PadicTateTwist.ext {p : ℕ} {K : Type u_1} [CommMonoid K] {x y : PadicTateTwist p K} (h : ∀ (n : ℕ), (proj n) x = (proj n) y) : x = y

A point of ℤ_p(1) is determined by all of its roots-of-unity components.

theorem TauCeti.PadicTateTwist.ext_iff {p : ℕ} {K : Type u_1} [CommMonoid K] {x y : PadicTateTwist p K} : x = y ↔ ∀ (n : ℕ), (proj n) x = (proj n) y

instance TauCeti.PadicTateTwist.instFiniteLevel {p : ℕ} {K : Type u_1} [NeZero p] [CommRing K] [IsDomain K] (n : ℕ) : Finite (TateModuleLevel p (Additive Kˣ) n)

For nonzero p, every finite level of the p-adic Tate twist over a domain is finite.

instance TauCeti.PadicTateTwist.instCompactSpace {p : ℕ} {K : Type u_1} [NeZero p] [CommRing K] [IsDomain K] : CompactSpace (PadicTateTwist p K)

For nonzero p, the p-adic Tate twist over a domain is compact in its inverse-limit topology.

theorem TauCeti.PadicTateTwist.natCard_tateModuleLevel {p : ℕ} {K : Type u_1} [CommMonoid K] [NeZero p] (n : ℕ) [HasEnoughRootsOfUnity K (p ^ n)] : Nat.card (TateModuleLevel p (Additive Kˣ) n) = p ^ n

If K has enough p ^ n-th roots of unity, then the n-th level of ℤ_p(1) has p ^ n elements.

theorem TauCeti.PadicTateTwist.nonempty_linearEquiv (p : ℕ) (K : Type u_1) [CommMonoid K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] : Nonempty (PadicTateTwist p K ≃ₗ[ℤ_[p]] ℤ_[p])

If K has enough p-power roots of unity, then ℤ_p(1) is noncanonically linearly equivalent to ℤ_p.

instance TauCeti.PadicTateTwist.free {p : ℕ} {K : Type u_1} [CommMonoid K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] : Module.Free ℤ_[p] (PadicTateTwist p K)

If K has enough p-power roots of unity, then ℤ_p(1) is a free ℤ_p-module.

instance TauCeti.PadicTateTwist.finite {p : ℕ} {K : Type u_1} [CommMonoid K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] : Module.Finite ℤ_[p] (PadicTateTwist p K)

If K has enough p-power roots of unity, then ℤ_p(1) is finitely generated over ℤ_p.

theorem TauCeti.PadicTateTwist.finrank (p : ℕ) (K : Type u_1) [CommMonoid K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] : Module.finrank ℤ_[p] (PadicTateTwist p K) = 1

If K has enough p-power roots of unity, then ℤ_p(1) has rank one over ℤ_p.

noncomputable def TauCeti.PadicTateTwist.galoisRepresentation {p : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fact (Nat.Prime p)] : Representation ℤ_[p] Gal(K/F) (PadicTateTwist p K)

The componentwise action of Gal(K/F) on the p-adic Tate twist.

Equations

• TauCeti.PadicTateTwist.galoisRepresentation = { toFun := fun (σ : Gal(K/F)) => TauCeti.TateModule.mapLinearMap (TauCeti.PadicTateTwist.unitsMap✝ σ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.PadicTateTwist.coe_tateModuleProj_galoisRepresentation {p : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fact (Nat.Prime p)] (σ : Gal(K/F)) (x : PadicTateTwist p K) (n : ℕ) : ↑(Additive.toMul ↑((TateModule.proj n) ((galoisRepresentation σ) x))) = σ ↑(Additive.toMul ↑((TateModule.proj n) x))

The Galois representation applies the field automorphism to every roots-of-unity component.

@[simp]

theorem TauCeti.PadicTateTwist.galoisRepresentation_apply_eq_smul {p : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] (σ : Gal(K/F)) (x : PadicTateTwist p K) : (galoisRepresentation σ) x = ↑((cyclotomicCharacter K p) σ.toRingEquiv) • x

When K contains all p-power roots of unity, the Galois action on ℤ_p(1) is scalar multiplication by the p-adic cyclotomic character.

theorem TauCeti.PadicTateTwist.continuous_galoisRepresentation {p : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Fact (Nat.Prime p)] [∀ (n : ℕ), HasEnoughRootsOfUnity K (p ^ n)] : Continuous fun (q : Gal(K/F) × PadicTateTwist p K) => (galoisRepresentation q.1) q.2

The Galois action on ℤ_p(1) is jointly continuous when all p-power roots of unity exist.

The ℓ-adic component of the prime-to-p Tate module

noncomputable def TauCeti.PrimeToPTateModule.toPadicTateTwist {p : ℕ} {E : Type u_1} [CommMonoid E] (ℓ : ℕ) [NeZero ℓ] (hℓ : ℓ.Coprime p) : PrimeToPTateModule p E →ₜ* Multiplicative (PadicTateTwist ℓ E)

The ℓ-adic component of the prime-to-p Tate module. For ℓ nonzero and prime to p, the powers ℓ ^ n are among the levels of ℤ̂^{(p')}(1) = lim_{p ∤ m} μ_m(E), and keeping only those components is a continuous homomorphism to the ℓ-adic Tate twist ℤ_ℓ(1) = lim_n μ_{ℓ ^ n}(E), written multiplicatively. For a prime ℓ ≠ p this is the specialization of ℤ̂^{(p')}(1) at the prime ℓ.

Equations

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

@[simp]

theorem TauCeti.PrimeToPTateModule.proj_toPadicTateTwist {p : ℕ} {E : Type u_1} [CommMonoid E] {ℓ : ℕ} [NeZero ℓ] {hℓ : ℓ.Coprime p} (x : PrimeToPTateModule p E) (n : ℕ) : (PadicTateTwist.proj n) (Multiplicative.toAdd ((toPadicTateTwist ℓ hℓ) x)) = Additive.ofMul ((proj ⟨ℓ ^ n, ⋯⟩) x)

The ℓ ^ n-th roots-of-unity component of the ℓ-adic component of x is the level-ℓ ^ n component of x.

theorem TauCeti.PrimeToPTateModule.toPadicTateTwist_smul {p : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] {hℓ : ℓ.Coprime p} (σ : Gal(K/F)) (x : PrimeToPTateModule p K) : (toPadicTateTwist ℓ hℓ) (σ • x) = Multiplicative.ofAdd ((PadicTateTwist.galoisRepresentation σ) (Multiplicative.toAdd ((toPadicTateTwist ℓ hℓ) x)))

The ℓ-adic component is Galois-equivariant: it carries the action of Gal(K/F) on ℤ̂^{(p')}(1) through the roots of unity to the Galois representation on ℤ_ℓ(1).