Simpler multiplication on circle Lemma 8.5.8

[Alizter]

I noticed that the book is describing the multiplication map in a pretty complicated way. Here is a simpler one that doesn't use funext which I found in the lean formalization.

I think it would be beneficial to define the map h mentioned in the book again here, since it is a bit annoying having to flick back. We can even give it a better name than h like the turn map or something.

turn : (x : S1) -> x = x, defined by induction on x. We map base to loop, so we need to show that transport (lambda x . x = x) loop loop = loop. By 2.11.2, we need to show (loop^-1 @ loop) @ loop = loop which is easy.

Next we want to define a map S1 -> S1 -> S1 (uncurry it if you like). Let x y : S1 we construct the element of S1 as S1-rec y (turn y) x.

This is much simpler, and avoids funext completely. Showing that S1 is a H-space is also much simpler now. And notably showing that this operation is associative is actually doable on paper.

[mikeshulman]

Thanks for this suggestion. But I'm divided about whether this is minor enough for a first-edition update. Anyone else have an opinion?

[awodey]

How about adding it as a Remark or Exercise?

Sent from my iPhone

On Nov 30, 2019, at 01:28, Mike Shulman notifications@github.com wrote:

Thanks for this suggestion. But I'm divided about whether this is minor enough for a first-edition update. Anyone else have an opinion?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[mikeshulman]

Yes, that's a good idea.

[Alizter]

I think it might be interesting to add a remark contrasting circle induction with say natural number induction here. Usually when proving things about the natural numbers, people get stuck because they didn't assume a general enough hypothesis, typically doing this every time is fine.

On the other hand, for the circle this might not work as intended, since as soon as you want to do induction on x for something like (x : S1) -> (y : S1) -> P x y, you will need to assume funext to prove transport (lambda x . (y : S1) -> P x y) loop base_P base_P. The better thing to do is to introduce x and y, swap x and y in the context, then induct on x.

It's true that funext will save the day and allow you to finish the proof, but you will be hard pressed to prove anything about your construction, since you will constantly have to reduce funext terms and make sure they don't break anything etc.