UniMath
4.9.4 Any symmetry is a symmetry in (was: of) Set
I do not exactly understand what this title means (or meant).
The message should be: any group is a group of permutations. Re first occurrence of "symmetry": this is rather an element of a group, not the group itself. Re second occurrence of "symmetry": this is rather an element of A=A for some A:Set.
It would help to have this example later, in the chapter about subgroups. Then we could say something closer to the message, for example, "Any group is a subgroup of the symmetries of a set."
This is always the same problem with the meaning of "is". Strictly speaking, a symmetry g of the shape sh in the groupoid G "is" only that, or potentially "is" any other symmetry of sh which is equal to g (as elements of sh=sh). Meaning that if "is" stands for "propositionally equal", then it makes no to "be" something which does not live in the same type.
Maybe "Any symmetry can be seen/considered as a symmetry of a set" would be less misleading. The formal correct phrasing is of course what you say: any group is a subgroup of the group of symmetries of a set. This is however a lot technical/verbose to convey the actual intuition behind the statement: any element of an abstract group is just a permutation in disguise.
Delaying this statement for after subgroups are introduced does not seem absolutely necessary, but maybe it is the best option if we want to avoid the shenanigans on talking about subgroups without mentioning subgroups.
It is not only that. There are two things that are more important (to me):
- A symmetry is defined (already from Ch.2 on) as an element of a=a for some a:A. This is more general that just A being the classifying type of a group, making the title technically wrong.
- Even with A the classifying type of a group, "any group element can be seen as the permutation of a set" is not very accurate.
Re: "any element of an abstract group is just a permutation in disguise."
I think "disguise" is not accurate here, for it implies that the permutation group is lurking already behind the scenes, whereas, it's something we introduce by artifice. Also "is" is not accurate, as you've accurately explained.
Why don't we opt for accuracy and just wait until we can say that any group is isomorphic to a subgroup of a permutation group?
Yes, "any element of an abstract group is just a permutation in disguise" does not make clear that the set that is permuted is the same for all elements of the group.
"Why don't we opt for accuracy and just wait until we can say that any group is isomorphic to a subgroup of a permutation group?" is also my favorite solution.
I didn't pay attention to your first point Marc, indeed this is very problematic.
I also agree with the rest of the arguments here, and we can postpone this paragraph. (Maybe @bidundas who wrote the section initially has some input.)
For what it worth, we can also rephrase as: every group acts faithfully on a set. And I think every term there is already defined at that point. But maybe it misses the point in that phrasing...
@bidundas has no input here. While keeping in mind that some of our readers may have different background than any of us do we want things to be both correct and digestible. Any outcome that meets both these criteria should be fine.
Best,
Bjorn
On Jul 15, 2020, at 14:44, Pierre Cagne [email protected] wrote:
I didn't pay attention to your first point Marc, indeed this is very problematic.
I also agree with the rest of the arguments here, and we can postpone this paragraph. (Maybe @bidundas who wrote the section initially has some input.)
For what it worth, we can also rephrase as: every group acts faithfully on a set. And I think every term there is already defined at that point. But maybe it misses the point in that phrasing...
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.
