UniMath
Circle chapter revamp (for discussion)
Here's something we can discuss today: In 0cf34b0 and earlier commits, I'm going through the circle chapter and thinking about what I'd like to change (and making lots of changes already: sorry!).
I took the old xca:coveringsofS1 and changed it to a theorem thm:coveringsofS1perms (now 3.3.6), which I feel should guide the whole chapter. In the “Reinterpretation” section, Sec. 3.5, I then introduce the type InfCyc, later also called Cyc₀, of infinite cycles.
In Sec. 3.6 (sec:covS1), I then introduce the type of all cycles, Def. 3.6.1 (def:Cyc), and prove they're equivalent to connected set bundles. I explicitly introduce the power bundle (can't really be the “power set bundle”, sigh), from the standard m-cycle, and prove it corresponds to the degree m function. The workhorse behind the symmetries of the degree m set bundle / cycle, is then Lem. 3.6.9 (lem:IdCycle). (Frankly, I was very confused by the old proof of thm:coveringsofS1, and I like this approach much better.) Note that Lem. 3.6.9 holds for all cycles, without assuming LPO.
Since we have Con. 2.21.4, we can have a shorter treatment of LPO than previously.
I like the name “cycle”, but it can of course be negotiated. I feel it paves the way nicely for permutation groups (which is still TBD).
I also considered “cyclically ordered set” and “cyclic set”, but these already mean something different, but are related.
Question: We'd like consistent variable names for bundles (A,f), (B,g), cycles (X,t), (Y,u), and families E, F. Are these good? Or maybe (X,σ), (Y,τ) instead, with σ,τ for permutations?
I put some more things to do in Sec. 3.8. I'm still editing the chapter, but discussion is very welcome, esp. during our meeting today!
Okay, but you have a missing " \end{align*} " at line 1666 of circle.tex.
Sorry, fixed in d30bb02
BTW, I moved the m-th root stuff to a new section, now Sec. 3.7. I like this a lot, but I felt it got in the way for the earlier parts, and I hope to give it its full due there, which includes discussion of its action on finite cycles (etc. as mentioned in the TODO section, cur. Sec. 3.8).
It might have been discussed already during a session I did not participated in, but is there a reason we went from the successor permutation to the predecessor permutation in defining the image of the loop in InfCyc ?
It might have been discussed already during a session I did not participated in, but is there a reason we went from the successor permutation to the predecessor permutation in defining the image of the loop in InfCyc ?
We briefly discussed it before: One reason is to get the right-hand triangle in (3.5.1) to commute via the winding-number, rather than its negation (as illustrated in Fig. 3.5). Another, and even better, reason is to make this exactly the special case of the generalization to finitely generated free groups. (This is still to be written, though.)
Perhaps something for discussion today: Lem. 3.6.11 (lem:cycle-order-point-ap) needed the winding number at an arbitrary point of the circle, so I added Ex. 3.4.8 (xca:general-winding). I hint (in a footnote) that we get a product on the circle. I don't think we have anywhere yet that the points of the circle form the elements of an oo-group with this product, but this would also be a natural thing to cover, maybe in Sec. 4.4?
I find myself at my office w/o my computer. Can someone help me out and send me a pdf of the book as it appears today?
Bjorn
On 18 Mar 2021, at 12:35, Ulrik Buchholtz @.***> wrote:
Perhaps something for discussion today: Lem. 3.6.11 (lem:cycle-order-point-ap) needed the winding number at an arbitrary point of the circle, so I added Ex. 3.4.8 (xca:general-winding). I hint (in a footnote) that we get a product on the circle. I don't think we have anywhere yet that the points of the circle form the elements of an oo-group with this product, but this would also be a natural thing to cover, maybe in Sec. 4.4?
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.
