This question is more about strategy, which can be used when developing group theory, then about a particular proofs.

$ \newcommand{GRP}{\mathsf{GRP}} \newcommand{SET}{\mathsf{SET}} $ One way to define free group $F_\GRP(A)$ for a set $A$ is to get construct it explicitly as $$ F_\GRP(A) = \frac{\bigcup^\infty_{n=0} (A \sqcup A)^n}{(\sim)} $$

as set of sequences of elements of $A$ with $+1$ or $-1$ sign quotiented by suitable equivalence relation. The bad thing about this approach is that it requires some busy lemmas on words to prove that resulting construction is indeed a group with a desired universal property.

On the other hand one can use some adjoint functor existence theorems to show that forgotful functor $U_\GRP : \GRP \to \SET $ indeed has a left adjoint which is $F_\GRP$. Now, as I know some category theory, I can use these theorems explicitly instead of inventing ad hoc versions of them. The drawback of this approach is that actual structure of free groups is somewhat obfuscated.

However, in my opinion this is not a problem, as left adjoints preserve colimits, and so I can write $$ F_\GRP(A) = F_\GRP\left(\bigsqcup_{a \in A}\{a\} \right) = \coprod_{a \in A} F_{\GRP}\{a\} = \coprod_{a \in A} \mathbb{Z}, $$ where coproduct sign stands for free product. So, to describe free groups I'm left with proving that the free group of the singleton is the countable cyclic group $\mathbb{Z}$, and getting and understanding free products.

But here I'm getting a similar problem, the constructive definition of free product of groups $(G_i)_{i \in I}$ is similarly $$ \coprod_{i \in I} G_i = \frac{\bigcup^\infty_{n=0}\left(\bigsqcup_{i \in I} U_{\GRP} (G_i) \right)^n}{(\sim)}, $$

which will require similar busy work with finite words. It is OK, and I can do it. But I still want to ask:

Is there an alternative way to define, prove existence and understand structure of free products of groups? I would prefer methods that use category theory to some extension.

  • 2
    $\begingroup$ How do you expect to understand the structure without dealing with words? Proving the mere existence is much easier, though (for instance see math.stackexchange.com/questions/2625783/…, or you can make an even easier proof by an adjoint-functor-theorem-like argument). $\endgroup$ – Eric Wofsey Aug 10 '18 at 21:06
  • 2
    $\begingroup$ To be more specific, you can prove that coproducts exist by applying the adjoint functor theorem to get a left adjoint to the diagonal functor $\GRP\to \GRP^I$. The solution set condition just amounts to verifying that there is only a small set of groups up to isomorphism which are generated by homomorphic images of the $G_i$. $\endgroup$ – Eric Wofsey Aug 10 '18 at 21:12
  • 3
    $\begingroup$ I won't make this an answer since you want a category theory method, but, you can do this using graphs and their universal covering trees, at least for free groups. For more general free products you can also do this with trees, although the technology is quite a bit more complicated. $\endgroup$ – Lee Mosher Aug 10 '18 at 22:27
  • 1
    $\begingroup$ Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $\operatorname{Red}(A)$, the set of reduced words on $A \sqcup \bar A$. Basically, for $x\in A$, it takes a word $w$ to $xw$ unless $w$ begins with $\bar x$ so $w = \bar x w'$, in which case it takes $w$ to $w'$. Then it turns out the free group is just the subgroup of the symmetric group generated by these permutations - and each reduced word $w$ sends the empty string to $w$ so they give distinct permutations. And associativity is automatic. $\endgroup$ – Daniel Schepler Aug 11 '18 at 0:42
  • 1
    $\begingroup$ A nonanswer and not really about reduced words, but you might be interested in "Topology of finite graphs" by Stallings where he (re)proves many interesting results about free group by understanding a certain category of graph. For example proving intersection of finitely generated subgroup of free groups is still fintely generated (by doing a "categorical intersection" in this category of graphs, which from what I remember of algebraic geometry is how you define intersection of schemes) $\endgroup$ – Paul Plummer Aug 11 '18 at 1:41

In general, if $\mathcal{A}$ is a variety of algebras and $U : \mathcal{A} \to \mathbf{Sets}$ is the forgetful functor, then we can construct a left adjoint $F : \mathbf{Sets} \to \mathcal{A}$ as follows:

  1. First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $\mathcal{A}$. (If you're using ZFC as your foundations, you will likely need a set-theoretic argument to show this can be represented by an actual set rather than a proper class.)

  2. Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $\mathcal{A}$ with formal expressions substituted in, and which also makes all the formal operations be respectful of the equivalence relation. (It is straightforward to show the class of relations on the set of formal expressions from (1) satisfying these requirements is closed under arbitrary intersections; so then, for example, you could construct the desired equivalence relation as the intersection of all such relations.)

Then, in many cases, it's possible to represent each equivalence class by a member of a restricted class of expressions which is easier to work with; and if we're lucky, we might even be able to choose a canonical such expression in each equivalence class.

In the case $\mathcal{A} = \mathbf{Groups}$, for example, it is easy to show that any formal expression from (1), modulo the equivalence relation in (2), is equivalent to a (possibly empty) product of elements $x \in X$ or $y^{-1}$ for $y \in X$ which together form a reduced word. You would prove this by "structural induction" on the general formal expression (or, if you prefer, by strong induction on the "total size" of the general formal expression). The harder part is to show that any two distinct reduced words end up in different equivalence classes.

To make this process more concrete in the group case, I think it might help to show how this would be encoded in Coq, where for example (1) is very similar to the way you would define an "abstract syntax tree" type in OCaml or Haskell:

(* formal expressions from (1) *)
Inductive free_group (X:Type) : Type :=
| fg_atom (x:X)
| fg_id
| fg_inv (x : free_group X)
| fg_mul (x y : free_group X).

Arguments fg_atom [X] x.
Arguments fg_id [X].
Arguments fg_inv [X] x.
Arguments fg_mul [X] x y.

(* Equivalence relation described in (2) *)
Inductive fg_equiv (X:Type) : free_group X -> free_group X -> Prop :=
| fg_left_id : forall x : free_group X,
  fg_equiv X (fg_mul fg_id x) x
| fg_right_id : forall x : free_group X,
  fg_equiv X (fg_mul x fg_id) x
| fg_left_inv : forall x : free_group X,
  fg_equiv X (fg_mul (fg_inv x) x) fg_id
| fg_right_inv : forall x : free_group X,
  fg_equiv X (fg_mul x (fg_inv x)) fg_id
| fg_mul_assoc : forall x y z : free_group X,
  fg_equiv X (fg_mul (fg_mul x y) z) (fg_mul x (fg_mul y z))
| fg_equiv_refl : forall x : free_group X,
  fg_equiv X x x
| fg_equiv_sym : forall x y : free_group X,
  fg_equiv X x y -> fg_equiv X y x
| fg_equiv_trans : forall x y z : free_group X,
  fg_equiv X x y -> fg_equiv X y z -> fg_equiv X x z
| fg_equiv_resp_id : fg_equiv X fg_id fg_id
| fg_equiv_resp_inv : forall x x' : free_group X,
  fg_equiv X x x' -> fg_equiv X (fg_inv x) (fg_inv x')
| fg_equiv_resp_mul : forall x x' y y' : free_group X,
  fg_equiv X x x' -> fg_equiv X y y' ->
  fg_equiv X (fg_mul x y) (fg_mul x' y').

(Incidentally, it's also very easy to extend this to describe the group with any given presentation, or in general the object of any variety of algebras with a given presentation: just add the relations from the presentation to the requirements on the equivalence relation in (2).)

  • $\begingroup$ The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for the fg_equiv relation. You've given a clearer approach yet it contains the same essential thorns. $\endgroup$ – Musa Al-hassy Aug 13 '18 at 17:57
  • $\begingroup$ @MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved by fg_mul_assoc . Where the "busy lemmas" come in is in the part I mentioned about proving that two different reduced words land in distinct equivalence classes. (And that's where "van der Waerden's trick" could come to the rescue: define a group homomorphism from the quotient to the symmetric group on the set of reduced words, then show the action of each reduced word sends the empty word to itself.) $\endgroup$ – Daniel Schepler Aug 13 '18 at 18:04
  • $\begingroup$ Interesting. I thought OP wanted a direct interface rather than an abstract one. Let me clarify, your approach could be mimicked for monoids to produce their term language as free monoid, yet it does not inform more than that. Whereas a direct interface would be lists. Why do you think it is that we have direct interfaces for monoids but not for groups? $\endgroup$ – Musa Al-hassy Aug 13 '18 at 18:07
  • $\begingroup$ Well, it's highly dependent on the variety of algebras you're considering, whether you can come up with a nice canonical description of the equivalence classes or not. For instance, I personally don't know of any such nice description for the category of Lie algebras - and similarly, for Heyting algebras, I think the Wikipedia article says there's no known "nice" description there either. As far as I know, there might even be concrete varieties where the word problem for free objects isn't decidable. So, we get "lucky" with monoids, groups, rings, commutative rings. $\endgroup$ – Daniel Schepler Aug 13 '18 at 18:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.