Re: [HoTT] Syllepsis in HoTT

[Noah Snyder <nsnyder@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4869 bytes --]

The generator of \pi_4(S^3) is the image of the generator of \pi_3(S^2)
under stabilization.  This is just the surjective the part of Freudenthal.
So to see that this generator has order dividing 2 one needs exactly two
things: the syllepsis, and my follow-up question about EH giving the
generator of \pi_3(S^2).  This is why I asked the follow-up question.

Note that putting formalization aside, that EH gives the generator of
\pi_4(S^3) and the syllepsis the proof that it has order 2, are well-known
among mathematicians via framed bordism theory (already Pontryagin knew
these two facts almost a hundred years ago).  So informally it’s clear to
mathematicians that the syllepsis shows this number is 1 or 2.  Formalizing
this well-known result remains an interesting question of course.

Best,

Noah


On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:

> Dear Noah,
>
> I don't think that your claim that syllepsis gives a proof that Brunerie's
> number is 1 or 2 is accurate. Syllepsis gives you that a certain element of
> pi_4(S^3) has order 1 or 2, but it is an entirely different matter to show
> that this element generates the group. There could be many elements of
> order 2.
>
> Best wishes,
> Egbert
>
> On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:
>
>> Hi Kristina,
>>
>> I've been on it already, because I was in that talk, and while my
>> formalization isn't yet finished, I do have all the pseudocode already.
>>
>> Best wishes,
>> Egbert
>>
>> On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
>>
>>> On the subject of formalization and the syllepsis, has it ever been
>>> formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?  That is,
>>> we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1}
>>> --EH--> surf^{-1} \circ surf -->  refl_refl_base, and we want to show that
>>> under the equivalence \pi_3(S^2) --> Z constructed in the book that this
>>> 3-loop maps to \pm 1 (which sign you end up getting will depend on
>>> conventions).
>>>
>>> There's another explicit way to construct a generating a 3-loop on S^2,
>>> namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH
>>> whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -->
>>> refl_refl_base, where I've suppressed a lot of associators and other
>>> details.  One could also ask whether this generator is the same as the one
>>> in my first paragraph.  This should be of comparable difficulty to the
>>> syllepsis (perhaps easier), but is another good example of something that's
>>> "easy" with string diagrams but a lot of work to translate into formalized
>>> HoTT.
>>>
>>> Best,
>>>
>>> Noah
>>>
>>> On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <
>>> sojakova.kristina@gmail.com> wrote:
>>>
>>>> Dear all,
>>>>
>>>> Ali told me that apparently the following problem could be of interest
>>>> to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>>>>
>>>> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
>>>> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.
>>>>
>>>> I just established the above in HoTT and am thinking of formalizing it,
>>>> unless someone already did it.
>>>>
>>>> Thanks,
>>>>
>>>> Kristina
>>>>
>>>> --
>>>> You received this message because you are subscribed to the Google
>>>> Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>>> To view this discussion on the web visit
>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com
>>>> .
>>>>
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg5AjiFOxBf%2BG6g8iW5ui30gXmQsgbEH31CCxSY%3DQVLybw%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 7138 bytes --]