The free pro-p group on one generator is ℤ_p

The free pro-p group on a one-element type and the additive group of the p-adic integers represent the same functor on pro-p groups: a continuous homomorphism out of either into a pro-p group P is the same thing as an element of P, the image of the generator. For the free group this is its universal property; for ℤ_[p] it is the p-adic power TauCeti.IsProP.padicPowHom. The two universal properties assemble into a topological group isomorphism freeProP p X ≃ₜ* Multiplicative ℤ_[p] carrying the generator to 1, whose inverse sends l to the p-adic power of the generator by l.

The free pro-p group on one generator is therefore topologically finitely generated of rank one. No product decomposition of the profinite integers is involved.

The generating type is taken in Type, the universe of ℤ_[p], because the universal property of freeProP p X only produces homomorphisms into pro-p groups of the universe of X.

Main definitions

• TauCeti.freeProP.equivPadicInt: the isomorphism freeProP p X ≃ₜ* Multiplicative ℤ_[p] for a one-element type X.

Main results

• TauCeti.freeProP.equivPadicInt_of, TauCeti.freeProP.equivPadicInt_symm_ofAdd: the isomorphism carries the generator to 1, and its inverse is the p-adic power of the generator.
• TauCeti.freeProP.commute_of_unique: the free pro-p group on one generator is commutative.
• TauCeti.freeProP.bijective_lift_of_not_isOfFinOrder, TauCeti.freeProP.nonempty_continuousMulEquiv_of_not_isOfFinOrder: a pro-p group topologically generated by an element of infinite order is free pro-p on one generator.
• TauCeti.topologicalGeneratorRank_freeProP_of_unique: the free pro-p group on one generator has topological generator rank one.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 3.3 and 4.3.

noncomputable def TauCeti.freeProP.equivPadicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] : freeProP p X ≃ₜ* Multiplicative ℤ_[p]

The free pro-p group on one generator is ℤ_p. The topological group isomorphism from freeProP p X, for a one-element type X, to the additive group of the p-adic integers, sending the generator to 1. Its inverse sends l to the p-adic power of the generator by l.

Equations

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

@[simp]

theorem TauCeti.freeProP.coe_equivPadicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] : ↑(equivPadicInt p X) = lift ⋯ fun (x : X) => Multiplicative.ofAdd 1

The isomorphism with ℤ_p is the lift of the map sending the generator to 1.

@[simp]

theorem TauCeti.freeProP.equivPadicInt_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] (x : X) : (equivPadicInt p X) (of x) = Multiplicative.ofAdd 1

The isomorphism with ℤ_p sends the generator to 1.

@[simp]

theorem TauCeti.freeProP.coe_equivPadicInt_symm (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] : ↑(equivPadicInt p X).symm = ⋯.padicPowHom (of default)

The inverse of the isomorphism with ℤ_p is the p-adic power homomorphism of the generator.

@[simp]

theorem TauCeti.freeProP.equivPadicInt_symm_ofAdd (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] (l : ℤ_[p]) : (equivPadicInt p X).symm (Multiplicative.ofAdd l) = ⋯.padicPow (of default) l

The inverse of the isomorphism with ℤ_p sends l to the p-adic power of the generator by l.

theorem TauCeti.freeProP.equivPadicInt_unique (p : ℕ) [Fact (Nat.Prime p)] (X : Type) [Unique X] (e : freeProP p X ≃ₜ* Multiplicative ℤ_[p]) (he : ∀ (x : X), e (of x) = Multiplicative.ofAdd 1) : e = equivPadicInt p X

The isomorphism with ℤ_p is the unique topological isomorphism carrying the generator to 1.

theorem TauCeti.freeProP.commute_of_unique {p : ℕ} [Fact (Nat.Prime p)] {X : Type} [Unique X] (y z : freeProP p X) : Commute y z

The free pro-p group on one generator is commutative, being isomorphic to ℤ_p.

theorem TauCeti.isTopologicallyFinitelyGenerated_freeProP_of_unique (p : ℕ) [Fact (Nat.Prime p)] {X : Type} [Unique X] : IsTopologicallyFinitelyGenerated (freeProP p X)

The free pro-p group on one generator is topologically finitely generated.

theorem TauCeti.topologicalGeneratorRank_freeProP_of_unique (p : ℕ) [Fact (Nat.Prime p)] {X : Type} [Unique X] : topologicalGeneratorRank (freeProP p X) = 1

The free pro-p group on one generator has topological generator rank one.

theorem TauCeti.topologicalGeneratorRankNat_freeProP_of_unique (p : ℕ) [Fact (Nat.Prime p)] {X : Type} [Unique X] (h : IsTopologicallyFinitelyGenerated (freeProP p X)) : topologicalGeneratorRankNat (freeProP p X) h = 1

The natural-number topological generator rank of the free pro-p group on one generator is one.

theorem TauCeti.freeProP.bijective_lift_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Unique X] {P : Type u} [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 ⇑(lift hP fun (x : X) => a)

A pro-p group topologically generated by an element of infinite order is free pro-p on one generator: the continuous homomorphism from freeProP p X sending the generator to a is bijective. It is surjective because a generates, and injective because both groups are the p-adic powers of their generators and the p-adic power map of a is injective.

theorem TauCeti.freeProP.nonempty_continuousMulEquiv_of_not_isOfFinOrder {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Unique X] {P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (ha : (Subgroup.closure {a}).topologicalClosure = ⊤) (hfin : ¬IsOfFinOrder a) : Nonempty (P ≃ₜ* freeProP p X)

A pro-p group topologically generated by an element of infinite order is topologically isomorphic to the free pro-p group on one generator, that is, to ℤ_p.