Free groups are residually finite (external)
ProvedChou.residuallyFinite_freeGroupEvery free group is residually finite: for every nontrivial element there is a homomorphism to a finite group not killing it.
import Mathlib
namespace Chou /-- p. 406 (external): free groups are residually finite. -/ theorem residuallyFinite_freeGroup (α : Type*) : Group.ResiduallyFinite (FreeGroup α) := by sorry end Chou
Read-back
What the Lean code literally says, in plain math · claude-fable-5-1
Read-back: the free group on any set is residually finite
The statement
Let be any set whatsoever (any type, in any universe; it may be empty, finite, or infinite of any cardinality). Let denote the free group on , with its usual group structure. Then
where the intersection ranges over all normal subgroups of of finite index.
Because the intersection of subgroups is again a subgroup and always contains , this is equivalent to the elementwise form:
or, contrapositively: for every with there exists a normal subgroup of of finite index with .
No hypothesis is placed on ; the only binder is itself, universally quantified.
What each ingredient means, spelled out
The free group . Its elements are equivalence classes of finite words in the alphabet , i.e. finite lists of pairs with and a boolean, where is read as the letter and as . Two words are identified when one can be obtained from the other by a finite chain (in either direction) of single reduction steps, a single step being the deletion of an adjacent pair from anywhere inside the word. The group operations are: identity the class of the empty word; product the class of the concatenation of representatives; inverse the class of the reversed word with every boolean flipped. When is empty, is the trivial group. The statement quantifies over this case too.
Subgroup of finite index. For a subgroup , the index of is defined as the number of left cosets of in , encoded as a natural number by the convention that the number is when the set of cosets is infinite (the encoding sends any infinite cardinality to ). " has finite index" is then, by definition, the assertion that this natural number is nonzero. Since the set of cosets is nonempty (it contains itself), this is exactly the assertion that is a finite set, i.e. that has finite index in the ordinary sense.
Normal subgroup. is normal when for every and every .
The family being intersected. The intersection is indexed by the collection of all pairs (subgroup of , proof that is normal and of finite index); two such data with the same underlying subgroup are the same index. So it is literally the intersection of the underlying sets of all finite-index normal subgroups. This family is never empty: the whole group is normal in itself and has index , so the intersection is over a nonempty family and equals the set of elements lying in every finite-index normal subgroup.
The right-hand side. is the trivial subgroup, whose underlying set is exactly . The equality is an equality of subgroups of , which (subgroups being determined by their underlying sets) is the same as equality of the two underlying sets.
Edge cases the quantifier includes
- : is trivial, every subgroup is , and the claim reduces to .
- a singleton: is infinite cyclic; the claim is that the intersection of all finite-index subgroups of (all subgroups are normal) is trivial.
- of arbitrary infinite cardinality: no finiteness or countability assumption is made on ; the claim is asserted for free groups of every rank.
Confirmed by the mission captain (proposal self-audit).