Let be a set and a positive integer. Formulate the notion of a free nilpotent group on of nilpotence class and prove it has the appropriate universal property with respect to nilpotent groups of class at most .
Define the group , where . (Exponents denoting higher commutator subgroups.)
We will now prove the following: If is a nilpotent group of class at most and is a set function, then there exists a unique group homomorphism extending .
To see this, recall from the universal property of free groups that there is a unique group homomorphism extending . Moreover, , since is nilpotent of class at most . Thus there is a unique group homomorphism such that ; identifying with , we can say that extends . This gives existence.
To see uniqueness, Note that any group homomorphism which extends is determined uniquely by , which is determined uniquely by .