Topological generators of a procyclic pro-p group

A pro-p group P topologically generated by a single element a is procyclic, and every element of P is a p-adic power a ^ l with l ∈ ℤ_[p] (TauCeti.IsProP.mem_topologicalClosure_closure_singleton_iff). This file identifies which of those powers again generate: for P nontrivial, a ^ u topologically generates P exactly when u is a unit of ℤ_[p], the non-unit powers lying in the pro-p Frattini subgroup. Consequently any two topological generators of a procyclic pro-p group differ by a unit exponent. A procyclic pro-p group is ℤ/pᵏ when its generator has finite order, and otherwise the p-adic power map of the generator is injective, so the group is a copy of ℤ_p (TauCeti.freeProP.nonempty_continuousMulEquiv_of_not_isOfFinOrder, in TauCeti.Topology.Algebra.Group.Profinite.Free.PadicInt).

This is the change-of-generator statement behind the power-series coordinates of the completed group algebra ℤ_p[[P]] of an infinite procyclic pro-p group: the coordinates attached to two topological generators a and a ^ u differ by the substitution X ↦ (1 + X) ^ u - 1.

Main results

• TauCeti.IsProP.topologicalClosure_closure_padicPow_eq_top_iff: if a topologically generates the nontrivial pro-p group P, then a ^ u does so exactly when u is a unit.
• TauCeti.IsProP.exists_isUnit_padicPow_eq_of_topologicalClosure_closure_eq_top: two topological generators of a procyclic pro-p group differ by a unit exponent.
• TauCeti.IsProP.padicPowHom_injective_of_not_isOfFinOrder, TauCeti.IsProP.padicPow_right_injective_of_not_isOfFinOrder: the p-adic power map l ↦ a ^ l is injective when a has infinite order.
• TauCeti.IsProP.padicPowEquiv: for a topological generator a of infinite order, the p-adic power map l ↦ a ^ l is a topological group isomorphism Multiplicative ℤ_[p] ≃ₜ* P.
• TauCeti.IsProP.exists_continuousMulEquiv_multiplicative_zmod_pow_of_isOfFinOrder: a pro-p group topologically generated by an element a of finite order is topologically isomorphic to a finite cyclic group ℤ/pᵏ, by an isomorphism carrying a to the generator 1.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 4.3.

theorem TauCeti.IsProP.padicPow_mem_proPFrattini_of_dvd {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {l : ℤ_[p]} (hl : ↑p ∣ l) (a : P) : hP.padicPow a l ∈ proPFrattini p P

A p-adic power with exponent divisible by p lies in the pro-p Frattini subgroup.

theorem TauCeti.IsProP.topologicalClosure_closure_padicPow_eq_top_iff {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] [Nontrivial P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (u : ℤ_[p]) : (Subgroup.closure {hP.padicPow a u}).topologicalClosure = ⊤ ↔ IsUnit u

A unit power of a topological generator is a topological generator, and nothing else is. If a topologically generates the nontrivial pro-p group P, then the p-adic power a ^ u topologically generates P if and only if u is a unit of ℤ_[p].

theorem TauCeti.IsProP.exists_isUnit_padicPow_eq_of_topologicalClosure_closure_eq_top {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a b : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hb : (Subgroup.closure {b}).topologicalClosure = ⊤) : ∃ (u : ℤ_[p]), IsUnit u ∧ hP.padicPow a u = b

Two topological generators of a procyclic pro-p group differ by a unit exponent: if a and b both topologically generate P, then b = a ^ u for a unit u of ℤ_[p].

Injectivity of the p-adic power map, and finite procyclic groups

theorem TauCeti.IsProP.padicPowHom_injective_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : ¬IsOfFinOrder a) : Function.Injective ⇑(hP.padicPowHom a)

The p-adic power map of an element of infinite order is injective: if a ^ l = 1 then l = 0, since no a ^ (pᵛ) is 1 (TauCeti.IsProP.eq_zero_of_padicPow_mem).

theorem TauCeti.IsProP.padicPow_right_injective_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : ¬IsOfFinOrder a) : Function.Injective (hP.padicPow a)

The p-adic exponent of an element of infinite order is determined by the power: for a of infinite order, a ^ l = a ^ l' forces l = l'.

theorem TauCeti.IsProP.padicPowHom_bijective_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : ¬IsOfFinOrder a) : Function.Bijective ⇑(hP.padicPowHom a)

The p-adic power map of a topological generator a of infinite order is bijective: it is injective by TauCeti.IsProP.padicPowHom_injective_of_not_isOfFinOrder, and its range is the closed subgroup generated by a.

noncomputable def TauCeti.IsProP.padicPowEquiv {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : ¬IsOfFinOrder a) : Multiplicative ℤ_[p] ≃ₜ* P

A procyclic pro-p group with a generator of infinite order is a copy of ℤ_p. If a topologically generates the pro-p group P and has infinite order, the p-adic power map l ↦ a ^ l is a topological group isomorphism from the additive group of ℤ_[p] onto P, sending 1 to a.

Equations

• hP.padicPowEquiv ha hfin = (MulEquiv.ofBijective (hP.padicPowHom a) ⋯).toContinuousMulEquiv ⋯

@[simp]

theorem TauCeti.IsProP.padicPowEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : ¬IsOfFinOrder a) (l : Multiplicative ℤ_[p]) : (hP.padicPowEquiv ha hfin) l = hP.padicPow a (Multiplicative.toAdd l)

The isomorphism TauCeti.IsProP.padicPowEquiv is the p-adic power map of the generator.

@[simp]

theorem TauCeti.IsProP.padicPow_padicPowEquiv_symm {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : ¬IsOfFinOrder a) (x : P) : hP.padicPow a (Multiplicative.toAdd ((hP.padicPowEquiv ha hfin).symm x)) = x

The inverse of TauCeti.IsProP.padicPowEquiv returns the p-adic exponent of an element with respect to the generator.

theorem TauCeti.IsProP.exists_continuousMulEquiv_multiplicative_zmod_pow_of_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : IsOfFinOrder a) : ∃ (k : ℕ) (e : P ≃ₜ* Multiplicative (ZMod (p ^ k))), e a = Multiplicative.ofAdd 1

A pro-p group topologically generated by an element a of finite order is a finite cyclic p-group, hence topologically isomorphic to ℤ/pᵏ for some k by an isomorphism carrying a to the generator 1: the cyclic subgroup generated by a is finite, hence closed, so it is the whole group.