UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
377 stars 22 forks source link

split the introduction? #122

Open DanGrayson opened 3 years ago

DanGrayson commented 3 years ago

As suggested by Marc, perhaps we should split the introduction into two parts, so a chapter on symmetries can occur earlier.

marcbezem commented 3 years ago

Yes. Here are some further remarks/questions.

bidundas commented 3 years ago

On Sep 6, 2021, at 11:04, Marc Bezem @.***> wrote:

Yes. Here are some further remarks/questions.

• We could explore the symmetries of (Z,s^n) for any natural number n. • We could address the question (of which I don't know the answer): can any finite group be represented as the group of symmetries of (Z,f) for some equivalence f: Z -> Z? A bit unsure what you intend to say here; if Z is the integers and f:Z->Z is an equivalence, then surely f is either id or -id and the type of equivalences is Z as discussed earlier. If you mean, "let Z be a (given concrete) group and f:Z->Z an equivalence, what is the component of f in the type of self-equivalences” then the answer is the center of the group, and so the group you want to capture has to be abelian, but if that is all you want you can start with that group and the identity. Perhaps this is off the mark.

If no, the follow up question is: • Which finite groups can be represented as the group of symmetries of (Z,f) for some equivalence f: Z -> Z? • Same questions for countable groups. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

DanGrayson commented 3 years ago

Maybe it's Z as a set, not as a group ...

marcbezem commented 3 years ago

Sure, Z as a set, so for n=0 we get the full permutation group of Z, for n=1 we get (modulo isomorphy) the group of integers, for n=2 we get the group whose name I forget (since I haven't read the name). Yet another example is f:Z->Z defined by f(2z) = 2z+1 and f(2z+1) = 2z. What is (Z,f) in this case? I don't know if it is interesting (enough) to pursue this in general, but the question is simple: what groups can one get in this way?

bidundas commented 3 years ago

In your example, with f(n)+(-1)^n, any permutation g:Z->Z that satisfies g(n)+(-1)^{g(n)}=g(n+(-1)^n) will fit the bill (i.e. an even input n and its successor give an adjacent pair g(n) and g(n)+(-1)^{g(n) as output). Thus, for an arbitrary permutation h:Z->Z, both g(2n)=2h(n) and g(2n)=2h(n)+1 will work, but that seems to be it.

Bjorn

On Sep 6, 2021, at 16:18, Marc Bezem @.***> wrote:

Sure, Z as a set, so for n=0 we get the full permutation group of Z, for n=1 we get (modulo isomorphy) the group of integers, for n=2 we get the group whose name I forget (since I haven't read the name). Yet another example is f:Z->Z defined by f(2z) = 2z+1 and f(2z+1) = 2z. What is (Z,f) in this case? I don't know if it is interesting (enough) to pursue this in general, but the question is simple: what groups can one get in this way?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

marcbezem commented 3 years ago

Can we get a finite group as the symmetries of (Z,f) for some symmetry f of the set Z at all?

bidundas commented 3 years ago

Without having checked any details

Z splits into orbits \sum_aO_a of the f-action, and each of the O_as will be cyclic. An equivalence can permute the orbits, but must preserve the cardinality of the orbit, so that the group of automorphisms respecting f will be a semidirect product of the form \sum_p \prod_a Oa=O{p(a)} where p is a permutation and Oa=O{p(a)} will be cyclic (and composition will be of the form (p,g)(q,h)=(pq,gh) where gh:Oa=O{pq a}. Since either an orbit have to be infinite or the number of orbits has to be infinite, this is not finite.

Bjorn

On Sep 6, 2021, at 16:53, Marc Bezem @.***> wrote:

Can we get a finite group as the symmetries of (Z,f) for some symmetry f of the set Z at all?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

UlrikBuchholtz commented 3 years ago

Exactly. In the case where the orbits are all the same, we get a wreath product C ≀ S, where C is the (cyclic) group corresponding to an orbit, and S is the symmetry group of the set of orbits. Indeed, the classifying type for a symmetric group wreath product, G ≀ S, is B(G ≀ S) = ∑(X : BS), (X → BG), where S is BAut(A) for some type A.

For f(z) = z + n, there are n infinite cycles, and we get ℤ ≀ Sₙ. For n = 2, this is not the infinite dihedral group, D∞ = ℤ ⋊ S₂. (This has as classifying type the type of undirected infinite cycles, where the S₂ projection is the type of directions or “ends” – of which there are two.)

For f the even/odd swapper, with f(2z) = 2z+1, f(2z+1)=2z), there are infinitely many orbits of size 2, so we get C₂ ≀ Aut(Z).

Exercise(****): Give a concrete description of the automorphism group of (Z,f), where f(z)=3z+1.

marcbezem commented 3 years ago

This latter f is not surjective, do I miss something?

So, even if all orbits have different finite cardinalities, we get that each orbit should be permuted cyclically, and there are uncountably many such permutations of Z.

UlrikBuchholtz commented 3 years ago

Yes, it's not surjective. I was thinking of (Z,f) as an element of ∑(A : U), (A → A). (The type of pairs of a type and a self-equivalence is a subtype of this type, so it's a slight generalization.)

Of course, the joke is that to “solve” the exercise (which is not precisely phrased), you'd need to solve the Collatz problem, I think.

UlrikBuchholtz commented 3 years ago

Sorry, I wrote the wrong exercise! It should be:

Exercise(****): Give a concrete description of the automorphism group of (Z,f), where f(z)=3z+1 for z odd and f(z) = z/2 for z even.

marcbezem commented 3 years ago

Yes, I suspected Collatz, but was thinking ∑(A : U), (A = A) :-)

Concerning the suitability of the examples, I'm not sure any more. I think in the interlude chapter between the split introduction, we cannot use too advanced algebra (which I don't know myself, but would like to learn). I did some naive elaboration for f(z) = z + 2. Any permutation g respecting f is characterized by g(0)=n and g(1)=m such that n+m is odd. The unit comes from the g=id and is of course (0,1). We have (p,q)(n,m) = (p+n,q+m-1) if n is even, and (p,q)(n,m) = (q+n-1,p+m) if n is odd. The inverse of (n,m) is (-n,-m+2) if n is even, and (-m+1,-n+1) if n=odd. Without the more advanced tools, one does not get much insight from this (I hope my calculations are OK; if not this just underlines the lack of insight :-). Of course there could be a better view that is still elementary.