Royal Road to Free Groups and Free Products
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
This question is more about strategy, which can be used when developing group theory, then about a particular proofs.
$
newcommandGRPmathsfGRP
newcommandSETmathsfSET
$
One way to define free group $F_GRP(A)$ for a set $A$ is to get construct it explicitly as
$$
F_GRP(A) = fracbigcup^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_GRPleft(bigsqcup_a in Aa right) = coprod_a in A F_GRPa = coprod_a in A mathbbZ,
$$
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 $mathbbZ$, 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 = fracbigcup^infty_n=0left(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.
group-theory category-theory definition free-groups free-product
asked Aug 10 at 20:59
Nik Pronko
827917
 |Â
show 10 more comments
up vote
1
down vote
favorite
This question is more about strategy, which can be used when developing group theory, then about a particular proofs.
$
newcommandGRPmathsfGRP
newcommandSETmathsfSET
$
One way to define free group $F_GRP(A)$ for a set $A$ is to get construct it explicitly as
$$
F_GRP(A) = fracbigcup^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_GRPleft(bigsqcup_a in Aa right) = coprod_a in A F_GRPa = coprod_a in A mathbbZ,
$$
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 $mathbbZ$, 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 = fracbigcup^infty_n=0left(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.
group-theory category-theory definition free-groups free-product
asked Aug 10 at 20:59
Nik Pronko
827917
2
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).
– Eric Wofsey
Aug 10 at 21:06
2
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
3
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.
– Lee Mosher
Aug 10 at 22:27
1
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
1
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)
– Paul Plummer
Aug 11 at 1:41
 |Â
show 10 more comments
up vote
1
down vote
favorite
up vote
1
down vote
favorite
This question is more about strategy, which can be used when developing group theory, then about a particular proofs.
$
newcommandGRPmathsfGRP
newcommandSETmathsfSET
$
One way to define free group $F_GRP(A)$ for a set $A$ is to get construct it explicitly as
$$
F_GRP(A) = fracbigcup^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_GRPleft(bigsqcup_a in Aa right) = coprod_a in A F_GRPa = coprod_a in A mathbbZ,
$$
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 $mathbbZ$, 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 = fracbigcup^infty_n=0left(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.
group-theory category-theory definition free-groups free-product
asked Aug 10 at 20:59
Nik Pronko
827917
This question is more about strategy, which can be used when developing group theory, then about a particular proofs.
$
newcommandGRPmathsfGRP
newcommandSETmathsfSET
$
One way to define free group $F_GRP(A)$ for a set $A$ is to get construct it explicitly as
$$
F_GRP(A) = fracbigcup^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_GRPleft(bigsqcup_a in Aa right) = coprod_a in A F_GRPa = coprod_a in A mathbbZ,
$$
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 $mathbbZ$, 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 = fracbigcup^infty_n=0left(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.
group-theory category-theory definition free-groups free-product
asked Aug 10 at 20:59
Nik Pronko
827917
edited Aug 11 at 16:25
asked Aug 10 at 20:59
Nik Pronko
827917
asked Aug 10 at 20:59
Nik Pronko
827917
asked Aug 10 at 20:59
Nik Pronko
827917
827917
2
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).
– Eric Wofsey
Aug 10 at 21:06
2
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
3
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.
– Lee Mosher
Aug 10 at 22:27
1
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
1
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)
– Paul Plummer
Aug 11 at 1:41
 |Â
show 10 more comments
2
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).
– Eric Wofsey
Aug 10 at 21:06
2
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
3
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.
– Lee Mosher
Aug 10 at 22:27
1
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
1
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)
– Paul Plummer
Aug 11 at 1:41
2
2
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).
– Eric Wofsey
Aug 10 at 21:06
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).
– Eric Wofsey
Aug 10 at 21:06
2
2
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
3
3
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.
– Lee Mosher
Aug 10 at 22:27
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.
– Lee Mosher
Aug 10 at 22:27
1
1
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
1
1
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)
– Paul Plummer
Aug 11 at 1:41
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)
– Paul Plummer
Aug 11 at 1:41
 |Â
show 10 more comments
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
In general, if $mathcalA$ is a variety of algebras and $U : mathcalA to mathbfSets$ is the forgetful functor, then we can construct a left adjoint $F : mathbfSets to mathcalA$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $mathcalA$. (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.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $mathcalA$ 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 $mathcalA = mathbfGroups$, 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).)
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for thefg_equivrelation. You've given a clearer approach yet it contains the same essential thorns.
– Musa Al-hassy
Aug 13 at 17:57
@MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved byfg_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.)
– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
In general, if $mathcalA$ is a variety of algebras and $U : mathcalA to mathbfSets$ is the forgetful functor, then we can construct a left adjoint $F : mathbfSets to mathcalA$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $mathcalA$. (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.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $mathcalA$ 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 $mathcalA = mathbfGroups$, 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).)
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for thefg_equivrelation. You've given a clearer approach yet it contains the same essential thorns.
– Musa Al-hassy
Aug 13 at 17:57
@MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved byfg_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.)
– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
add a comment |Â
up vote
1
down vote
accepted
In general, if $mathcalA$ is a variety of algebras and $U : mathcalA to mathbfSets$ is the forgetful functor, then we can construct a left adjoint $F : mathbfSets to mathcalA$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $mathcalA$. (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.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $mathcalA$ 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 $mathcalA = mathbfGroups$, 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).)
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for thefg_equivrelation. You've given a clearer approach yet it contains the same essential thorns.
– Musa Al-hassy
Aug 13 at 17:57
@MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved byfg_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.)
– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
In general, if $mathcalA$ is a variety of algebras and $U : mathcalA to mathbfSets$ is the forgetful functor, then we can construct a left adjoint $F : mathbfSets to mathcalA$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $mathcalA$. (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.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $mathcalA$ 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 $mathcalA = mathbfGroups$, 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).)
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
In general, if $mathcalA$ is a variety of algebras and $U : mathcalA to mathbfSets$ is the forgetful functor, then we can construct a left adjoint $F : mathbfSets to mathcalA$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $mathcalA$. (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.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $mathcalA$ 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 $mathcalA = mathbfGroups$, 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).)
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
answered Aug 13 at 17:08
Daniel Schepler
6,9631514
6,9631514
The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for thefg_equivrelation. You've given a clearer approach yet it contains the same essential thorns.
– Musa Al-hassy
Aug 13 at 17:57
@MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved byfg_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.)
– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
add a comment |Â
The "busy lemmas" that OP mentioned now take the form of congruence proof obligations for thefg_equivrelation. You've given a clearer approach yet it contains the same essential thorns.
– Musa Al-hassy
Aug 13 at 17:57
@MusaAl-hassy Actually, it's trivial to show that the quotient defines a group - for example, associativity of multiplication is directly proved byfg_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.)
– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
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.– Musa Al-hassy
Aug 13 at 17:57
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.– Musa Al-hassy
Aug 13 at 17:57
@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.)– Daniel Schepler
Aug 13 at 18:04
@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.)– Daniel Schepler
Aug 13 at 18:04
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?
– Musa Al-hassy
Aug 13 at 18:07
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?
– Musa Al-hassy
Aug 13 at 18:07
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.
– Daniel Schepler
Aug 13 at 18:21
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.
– Daniel Schepler
Aug 13 at 18:21
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2878807%2froyal-road-to-free-groups-and-free-products%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
2
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).
– Eric Wofsey
Aug 10 at 21:06
2
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 $GRPto 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$.
– Eric Wofsey
Aug 10 at 21:12
3
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.
– Lee Mosher
Aug 10 at 22:27
1
Another construction (which was introduced to me as "van der Waerden's trick") is to identify each element of $A$ with a permutation of $operatornameRed(A)$, the set of reduced words on $A sqcup bar A$. Basically, for $xin 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.
– Daniel Schepler
Aug 11 at 0:42
1
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)
– Paul Plummer
Aug 11 at 1:41