Torsion in the p-adic completion of a multiplicative group

For a prime p and a field L, this file computes the torsion of the completed multiplicative module A(L) = lim_m Lˣ/(Lˣ)^(p^m) of TauCeti.padicCompletionUnits: it is exactly the image of the p-power roots of unity of L. Every level Lˣ/(Lˣ)^(p^m) has exponent dividing p^m, so A(L) has no torsion prime to p; an element killed by p^j is, at every level, the class of a p^j-th root of unity, and since there are only finitely many of those a single root of unity represents it at all levels simultaneously.

When the p-power roots of unity of L are finite (for instance when L is a finite extension of ℚ_p, by TauCeti.finite_pPowerRootsOfUnity), they embed into A(L), so the torsion of A(L) is finite of order q(L) = TauCeti.localRootOfUnityOrder. Finally, the torsion of A(L) as a ℤ_p-module is the torsion of the underlying multiplicative group: being killed by a nonzero p-adic integer is being killed by a power of p.

Main results

• TauCeti.padicCompletionUnits_pow_eq_one_iff: an element of A(L) is killed by p^j exactly when it is the class of a p^j-th root of unity.
• TauCeti.torsion_padicCompletionUnits: the torsion subgroup of A(L) is the image of TauCeti.pPowerRootsOfUnity p L.
• TauCeti.padicCompletionUnitsOf_injOn_pPowerRootsOfUnity: finitely many p-power roots of unity embed into A(L).
• TauCeti.natCard_torsion_padicCompletionUnits: the torsion of A(L) has order q(L).
• TauCeti.mem_torsion_padicCompletionUnits_iff: the ℤ_p-torsion submodule of A(L) is the additive form of its group torsion.
• TauCeti.mem_pPowerTorsion_padicCompletionUnits_iff, TauCeti.natCard_pPowerTorsion_padicCompletionUnits: the p-power torsion submodule of A(L), over any ring acting on it (such as ℤ_p[Gal(L/K)]), is the additive form of its group torsion, of order q(L).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, §VII.4.

theorem TauCeti.padicCompletionUnits_pow_eq_one_iff (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (x : ↥(padicCompletionUnits p L)) (j : ℕ) : x ^ p ^ j = 1 ↔ x ∈ Subgroup.map (padicCompletionUnitsOf p L) (rootsOfUnity (p ^ j) L)

An element of A(L) is killed by p^j exactly when it is the class of a p^j-th root of unity of L.

theorem TauCeti.torsion_padicCompletionUnits (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] : CommGroup.torsion ↥(padicCompletionUnits p L) = Subgroup.map (padicCompletionUnitsOf p L) (pPowerRootsOfUnity p L)

The torsion subgroup of A(L) is the image of the p-power roots of unity of L.

theorem TauCeti.padicCompletionUnitsOf_injOn_pPowerRootsOfUnity (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p L)) : Set.InjOn ⇑(padicCompletionUnitsOf p L) ↑(pPowerRootsOfUnity p L)

When L has only finitely many p-power roots of unity, they map injectively to A(L): a p-power root of unity that is a p^m-th power for every m is trivial.

theorem TauCeti.natCard_torsion_padicCompletionUnits (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p L)) : Nat.card ↥(CommGroup.torsion ↥(padicCompletionUnits p L)) = localRootOfUnityOrder p L h

When L has only finitely many p-power roots of unity, the torsion of A(L) has order q(L), the order of the group of p-power roots of unity of L.

theorem TauCeti.finite_torsion_padicCompletionUnits (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p L)) : Finite ↥(CommGroup.torsion ↥(padicCompletionUnits p L))

When L has only finitely many p-power roots of unity, the torsion of A(L) is finite.

theorem TauCeti.mem_torsion_padicCompletionUnits_iff (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (x : Additive ↥(padicCompletionUnits p L)) : x ∈ Submodule.torsion ℤ_[p] (Additive ↥(padicCompletionUnits p L)) ↔ Additive.toMul x ∈ CommGroup.torsion ↥(padicCompletionUnits p L)

The ℤ_p-torsion submodule of A(L) is the additive form of its group torsion: an element is killed by a nonzero p-adic integer exactly when it has finite multiplicative order.

theorem TauCeti.mem_pPowerTorsion_padicCompletionUnits_iff (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] {A : Type u_2} [Semiring A] [Module A (Additive ↥(padicCompletionUnits p L))] (x : Additive ↥(padicCompletionUnits p L)) : x ∈ pPowerTorsion p A (Additive ↥(padicCompletionUnits p L)) ↔ Additive.toMul x ∈ CommGroup.torsion ↥(padicCompletionUnits p L)

The p-power torsion of A(L), as a submodule over any ring acting on it, is the additive form of its group torsion: every element of finite order has p-power order.

theorem TauCeti.natCard_pPowerTorsion_padicCompletionUnits (p : ℕ) (L : Type u_1) [Field L] [Fact (Nat.Prime p)] (A : Type u_2) [Semiring A] [Module A (Additive ↥(padicCompletionUnits p L))] (h : Finite ↥(pPowerRootsOfUnity p L)) : Nat.card ↥(pPowerTorsion p A (Additive ↥(padicCompletionUnits p L))) = localRootOfUnityOrder p L h

When L has only finitely many p-power roots of unity, the p-power torsion of A(L), as a submodule over any ring acting on it, has order q(L).