Free groups are residually p

For every prime p, a nontrivial element of a free group survives in some finite p-group quotient. This is the classical residual p-finiteness of free groups; it is what makes the generators of a free pro-p group behave like free generators, and it gives residual finiteness of free groups as a special case.

Main results

• FreeGroup.exists_normal_isPGroup_quotient_notMem: a nontrivial element of FreeGroup X lies outside some normal subgroup of finite index whose quotient is a p-group.
• FreeGroup.instResiduallyFinite: free groups are residually finite.

References

• W. Magnus, Beziehungen zwischen Gruppen und Idealen in einem speziellen Ring, Math. Ann. 111 (1935), for the embedding of a free group in a ring of noncommutative power series.
• K. Iwasawa, Einige Sätze über freie Gruppen, Proc. Imp. Acad. Tokyo 19 (1943), for the residual p-finiteness of free groups.

theorem FreeGroup.exists_normal_isPGroup_quotient_notMem {X : Type u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] {w : FreeGroup X} (hw : w ≠ 1) : ∃ (N : Subgroup (FreeGroup X)) (x : N.Normal), N.FiniteIndex ∧ IsPGroup p (FreeGroup X ⧸ N) ∧ w ∉ N

Free groups are residually p. A nontrivial element of a free group lies outside some normal subgroup of finite index whose quotient is a p-group.

instance FreeGroup.instResiduallyFinite {X : Type u_1} : Group.ResiduallyFinite (FreeGroup X)

Free groups are residually finite.