The discrete free group embeds in the free pro-p group

For a prime p, the canonical homomorphism FreeGroup X →* freeProP p X is injective. This is the residual p-finiteness of free groups, FreeGroup.exists_normal_isPGroup_quotient_notMem, read through the universal property of freeProP p X: a finite p-group quotient of FreeGroup X is a discrete pro-p group, so the quotient map factors through freeProP p X. In particular the generators of the free pro-p group satisfy no relation of the discrete free group.

Through this embedding, the free pro-p group inherits the non-nilpotency of free groups of rank at least two (FreeGroup.lowerCentralSeries_ne_bot): in rank at least two no term γ_n of the lower central series of freeProP p X is trivial, and neither is any term of its closed lower central series, which contains it. So although the closed lower central series of a pro-p group has trivial intersection (TauCeti.IsProP.iInf_closedLowerCentralSeries_eq_bot), for a free pro-p group of rank at least two it never reaches ⊥ at a finite stage.

Main results

• TauCeti.freeProP.fromFreeGroup_injective: the discrete free group injects into the free pro-p group.
• TauCeti.freeProP.lowerCentralSeries_ne_bot, TauCeti.freeProP.closedLowerCentralSeries_ne_bot: in rank at least two, no term of the lower central series or of the closed lower central series of the free pro-p group is trivial.
• TauCeti.freeProP.not_isNilpotent: a free pro-p group of rank at least two is not nilpotent.

theorem TauCeti.freeProP.fromFreeGroup_injective {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} : Function.Injective ⇑(fromFreeGroup p X)

Free groups are residually p. The canonical homomorphism from the discrete free group on X to the free pro-p group on X is injective.

theorem TauCeti.freeProP.lowerCentralSeries_ne_bot {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Nontrivial X] (n : ℕ) : ⊤.lowerCentralSeries n ≠ ⊥

The lower central series of a free pro-p group of rank at least two never vanishes. The discrete free group embeds in freeProP p X, and the image of each term of its lower central series, which is never trivial, lies in the corresponding term for freeProP p X.

theorem TauCeti.freeProP.not_isNilpotent {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Nontrivial X] : ¬Group.IsNilpotent (freeProP p X)

Free pro-p groups of rank at least two are not nilpotent.

theorem TauCeti.freeProP.closedLowerCentralSeries_ne_bot {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Nontrivial X] (n : ℕ) : closedLowerCentralSeries (freeProP p X) n ≠ ⊥

The closed lower central series of a free pro-p group of rank at least two never vanishes. Each term γ_n contains the corresponding term of the lower central series of the underlying abstract group, which is nontrivial by TauCeti.freeProP.lowerCentralSeries_ne_bot.