UniMath
symmetry of \Set
We have this:
I was going to change the second phrase to "any symmetry is a symmetry of a set", since a symmetry of \Set would be a path from \Set to \Set in the next universe, but it's still not a good translation of the first phrase, which refers to a symmetry group, not to one symmetry in it.
Actually, the first phrase should really be "any group is a subgroup of a permutation group", so it's not clear what the corresponding phrase should be here. Maybe none.
I think both of them are mine. The duplication came from the monomorphism affair and one of them is to be deleted once people are happy.
Bjorn
On Apr 14, 2020, at 16:25, Daniel R. Grayson [email protected] wrote:
@bidundas - I think that text (at least one of them) is yours.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.
It looks like the later version is the good one and the first one can be deleted, because the later version comes after a discussion of monomorphisms and epimorphisms of groups.
This and many of your (Dan's) following comments were on my agenda in my planned rewriting of the material after the (last) monomorphism section (the first was to be deleted pending Marc’s approval).
I must admit that I have a problem with handling to a hoard of individual messages. Old fashioned as I am, I’d have preferred to have pages filled with (red) comments waiting for me when I’m done proofreading chapter 2 (which I plan to give a similar collected markup of). Alternatively, you seem to have a general outlook quite similar to my own so I won’t object if you want to take responsibility of the subgroup chapter.
Bjorn
On Apr 14, 2020, at 23:23, Daniel R. Grayson [email protected] wrote:
It looks like the later version is the good one and the first one can be deleted, because the later version comes after a discussion of monomorphisms and epimorphisms of groups.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.
Oh, I'm happy to do it that way, too -- I like marking things up in red and letting others make the changes. I will take a break from proofreading. I could look into expanding Chapter 9 on Euclidean geometry if you think that would be useful -- symmetry groups of objects, regular polyhedra, crystal structure, something like that.
I wasn't aware that things depended on my approval, which is flattering, but can hamper progress from time to time. Please delete the experimental stuff in 4.6. Regarding 4.9, here come some comments.
-
Lemma 4.9.1 (2) "injection" ---> surjection; immediately after that: (1) "given" ---> gives an; and in (2) the first B must be C.
-
First para after Def. 4.9.2, "we can let the source vary over any F:" is unclear. First, "source" is not defined, and, second, explanation after the ":" is missing. I think this argument is implicitly using the naturality (Lemma {lem:Znatural}, currently 4.3.9, may have changed) in G of the equivalence Hom(Z,G) -> UG. This would also simplify the argument (no need to mention Hom^abs(,)). Just look at the diagram of Lemma {lem:Znatural} and observe that the left vertical arrow there is post-composition by f, and the right vertical arrow is f^abs (both in deprecated notation, currently). Since the horizontal ='s are bijections we get (1)->(2).
-
Footnote 24 starts in a non-grammatical way, we could change: "and" ---> let. However, now that this material comes late in the chapter, (2)->(1) can be proved in a much simpler way: if fg=fh, then f^abs g^abs = f^abs h^abs, so by (2) and Lemma 4.9.1 (1) we get g^abs = h^abs, hence g=h.
