Eckmann-Hilton Updates

[morphismz]

Fixes links and makes consistent naming changes related to the Eckmann-Hilton file. Also adds an updated reference to the page.

[VojtechStep]

Thanks for the update. I didn't yet go through the content in detail, so this is a preliminary review

[fredrik-bakke]

Hey Raymond, welcome back! It's good to see you're active again. Looking forward to seeing what's coming next. 🙂

[morphismz]

Hey Raymond, welcome back! It's good to see you're active again. Looking forward to seeing what's coming next. 🙂

Hey Fredrik, thanks! I'm spinning up for the summer, hoping to get a good chunk of math formalized. Hoping to get the Hopf fibration finally all formalized. I figured I'd acquaint myself with the updates to the library by making a few small prs first. Though it seems like I should reacquaint myself with the style guide first 😄

[morphismz]

I've added a bit more work to this pr. The main result is a finished computation of transporting along an eckmann-hilton identification, resolving one of the tasks in issue #702 .

There is a bit more clean up I need to do before this pr is ready for review. I'll mark it ready when the time comes.

[morphismz]

I think this pr is now ready for review. There is one more lemma I will add later, namely computing transport along the eckmann-hilton 3-loop. But this relies on some infrastructure related to 3-automorphisms that I will be building in a different pr. So that lemma will wait.

Please let me know if I should tone down the prose, I feel like there is a lot on the Eckamnn-Hilton page. I added a bit of an explanation of how we compute transport along an Eckmann-Hilton identification. Let me know if there should be more or less of an explanation

[VojtechStep]

Great work! Those coherences look like a major PITA, so good job. I'd say 95% of my comments are just formatting. I think this amount of prose is very reasonable, it's always better to have more than less, and most of the content on that page is taken by arguments to lemmas which would be implicit in an ideal world. Keep it up!

[morphismz]

Those coherences look like a major PITA

Yes, yes they were...

Thanks for the diligent review process and all the feed back!

[morphismz]

Okay, I tried messing around with the diagrams a bunch, but I couldn't get anything to look nice. I'll delete them for now, so this pr can get merged. I'll keep thinking about ways to explain those coherence (maybe linking to some external diagrams, idk). If I come up with something, I'll add that in another pr.

But, for now, I figured, I'll just try to get this pr merged.

[VojtechStep]

Looks great, don't worry about the diagrams. I found a few typos, once those are fixed I'll merge the PR

[morphismz]

brother, you'd think I'd know how to spell concatenation by now

[morphismz]

Thanks for all the help on this pr @VojtechStep , and sorry again for the quite drawn out process

[VojtechStep]

My pleasure, and no worries, my schedule was also pretty tight, so I'd say the drawing-out was mutual 😅