From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 4562 invoked from network); 8 Mar 2021 13:38:21 -0000 Received: from mail-pg1-x53b.google.com (2607:f8b0:4864:20::53b) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 13:38:21 -0000 Received: by mail-pg1-x53b.google.com with SMTP id 2sf5662989pgo.0 for ; Mon, 08 Mar 2021 05:38:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615210698; cv=pass; d=google.com; s=arc-20160816; b=RbCBCO8w5H6CuY/Bzn8K9OL8yMpE1tzoexc4NgvN/dcgGU1Dqi6pEsBVaKtoDbsLFT LKaS9QOrKC9jo/2htoyq33N0pB3tmZhx0kmK+N2PbgOFLYkGt0nMJOK3+zVKQLTLvRir +A1CwJtvv4pqWeFhggehL7pnOAOFS5BCfEZlF+n8uUNQ15Em57uw3GBeO2cSzvIKv5Ep oREvBCP5aK2FCx8rKhSQmByVso49QnPnPcqt6inl0eEqiLSlD68PCaoIsSpvRFHRs2n2 jyuR5uocLBDQssIP/uCZGTlheFy8GEdP9MWKsOba6OEyS5Xe34EzYJN2/XkF12dO8e43 q0AA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=JfAQKxTF7nBs5610/CO5JVGSY6BjZ0ytLxxTyVtnvtI=; b=GhrEBHhPZ8rISWdzvTNS/tN1CWKixQ+/6gamy9Nj/4rPx7JzMFpLtFNQUuu7EkKqPe jn360IQFQYnbO6MaZq+ctx/FJa6rvfgo9bFErke+bHG49Zncl6ANfORVo0v9VBMD1JUl cFBMzX1JmuW+mwQU6mCSiTLMcsl51tIspFyNZkUCE8AJVhjsWhb0DCtl5l/duj2ph7xx r5eay7UMayDy3aeFGO01MOaVHX70Jx+H0JRXJFWKUBvY1zgnX1upw2tS/KtL5sqVNaVK JfIDanALZm3IwPWbdT4g1LLo3eqItmFgwqVFshxhBZJusgYwfEkxF8Ee3eAyL7jAv9Wv A2eg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=icYzgKPQ; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2b as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=JfAQKxTF7nBs5610/CO5JVGSY6BjZ0ytLxxTyVtnvtI=; b=DMNk18j0rF43zfMHK7c8k4j2uaJwSxEH+OHpIXbsIskQMTDa9El9a4aVQJ9ngRyEKz +01OPQwTOB4PWUn+4h3220TD7aIEGF56+LHHVWxNbZI+VS9bjRv4bdE6fy5SDkmaF6YH uBbgZD6niKmeFzc8bVouQtWVaXiaJ8BSVmUE0743igwVbRAhuZmrQJSIaFllWeONibMk oLyD66E2SizmoqWfjouUy8oTgpq7mX60GRfTIm5LySU9uyFC/atiWTu+OUlNuu90h4gP 6BZTV0nd8Ka7BNNAKzxSM2v+K0C3pGOb4Dlj2thBnepvK9/rIO4hUE5fxGZX5cfQmuBq dnww== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=JfAQKxTF7nBs5610/CO5JVGSY6BjZ0ytLxxTyVtnvtI=; b=TRvOtNX7ZuOG7687scRQXUP593pIbS6k5ErkhBAr2lKW4LL9Z1WGpJk4OKeMu34dJ2 /QQsS8qlnPGT/vTFoPiSA4K1Gyn0x7PwrLYqGa3vTCsos/BpaZJk/Jzd8DsoGCl7xk5E qPj+od0hkN6M3mb+UIuJIUjjqbxNE/f2J0BnN/pUIUCfRz0i8qGRSsjCYFzx9CYXz4dS CXgVMPmUy/QzqaATejDUJJOj9e1OddOuo+MO76MxvurGYIUKDJcdCOC9prOvp7LCbBoT oEJGpmDlvju/iwpicfWA+2JFqtxgron6Pgw+r2M4qrBhze4wnFve1r2Hz7cghtmhqnQ5 cWyQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=JfAQKxTF7nBs5610/CO5JVGSY6BjZ0ytLxxTyVtnvtI=; b=rLoHmaHuF9qYDSyUVQiOFRPJGSguty+qBhqTC6QtCVS3gJLpNnUnND/hcp8OhZc6X4 1zFiVuqbTYx58O9EWSHDRLUOX+sUf1dvq/CbdUV80oYicgvKxQb/okE8E8i7u1/Qz77I 5WN1Koi+I4Hx3AU9A1cqNLvS9nSQlX04OEXW7CKIldcNWgZX3ByNVwP+IP7DEOUL57ZJ 9JNotMCnk3+sLc8cxKo67YEu6Aj2XbKOYt/t3NChRH/n0sjNcN8oiAjKMeBhgB04MLml e/kjQIk/a/il6ZucxI8XxA0iiXWCrh6nlCGSGeqP31pPJYv1fhG1WnBJ1nPGGGoI5LCi geGA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530FqCpkMYz1IPejZv/iAGKO/vsxC0IXoNZGvPlpVo8ykFFdmPtv IFOq+S22NvM+UHBBPuQ8dq0= X-Google-Smtp-Source: ABdhPJxAFvBCM2ys9b7n0agRldWVYlJRRQX5x6s9q5TSKda0kZ/oEcHJd8po663NRZpkjs3dzjHaNg== X-Received: by 2002:a17:90a:bd06:: with SMTP id y6mr23485579pjr.112.1615210697550; Mon, 08 Mar 2021 05:38:17 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:2c8c:: with SMTP id s134ls6932285pfs.6.gmail; Mon, 08 Mar 2021 05:38:17 -0800 (PST) X-Received: by 2002:a62:184b:0:b029:1f4:4f14:5c1c with SMTP id 72-20020a62184b0000b02901f44f145c1cmr7811921pfy.77.1615210696890; Mon, 08 Mar 2021 05:38:16 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615210696; cv=none; d=google.com; s=arc-20160816; b=HmiO3mvOeb0nS2/Odim8//YwTqgeZPPAoAmvJbA4nOLC/6kPhemw4b4Px6vCMNSFih WAYA+dfyCqiPe1pu6jst1h8I/CHws1H254RYghXbV8Lt74b+U4oOc/3eHgke+m0njDMg z68/bL2HF//X8iSUx9aN+n5gQ6lSjb4tlC59AiiBhyF2NqddLSKIhJqMK8CeRo1QjMdu 2BJYZGSMiH1oG9A4hoAUD8U2HAT8oWslk9lWquiRNOCa1BuCk9nTzT3Pl0teabt1gOEY pma8k5ZOt4DMchZaqJ7TQhFA+NmK+CM9IGZUUpIYWWg9pF8SlH4CI31bBd/qCtjOzeLd 2MYQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=bYbzfmMo6rP84k4leYGbWyD26ud3GBRCqJhhRjTPGIM=; b=k82zZaO0tEbX0q5/fAnfrIfV9/bqBNq3asyg6tNCG4kQuusVxpZO7fm5h68t4mRIZY dHE8A7yjnoVfQ/CR6oxuLZB2qFalTvt/g8vDryduDsEDCyhUH4NO9IdZr7p8YuwR3P61 ig7NBiT8z5a7nuxT0dtcP3TtWzhMlGVDH32Sxjbfx0StD2IVl2W2V2Ur1pkKU7VLi8G0 D1drKMxm0mjLs32xAbIfRMylTyECipMAVfz7bosEIgQJWOLpIDNsTXqMbreQVV/AKRbQ J0XzFrXIY1roApeXxLwkWmVK8KnglrSV1AOIM/XpeXht9VnlDWeeADDHqWmXPlFuWGGP brdw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=icYzgKPQ; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2b as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe2b.google.com (mail-vs1-xe2b.google.com. [2607:f8b0:4864:20::e2b]) by gmr-mx.google.com with ESMTPS id e8si580142pgl.0.2021.03.08.05.38.16 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 05:38:16 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2b as permitted sender) client-ip=2607:f8b0:4864:20::e2b; Received: by mail-vs1-xe2b.google.com with SMTP id p24so4806912vsj.13 for ; Mon, 08 Mar 2021 05:38:16 -0800 (PST) X-Received: by 2002:a67:ff91:: with SMTP id v17mr12645836vsq.38.1615210696009; Mon, 08 Mar 2021 05:38:16 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> In-Reply-To: From: Noah Snyder Date: Mon, 8 Mar 2021 08:38:05 -0500 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Egbert Rijke Cc: Homotopy Type Theory , Kristina Sojakova Content-Type: multipart/alternative; boundary="000000000000c5e9c505bd068b15" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=icYzgKPQ; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2b as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000c5e9c505bd068b15 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=E2=80=99s cl= ear 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 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 sho= w > 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 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 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 t= hat >>> under the equivalence \pi_3(S^2) --> Z constructed in the book that thi= s >>> 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 th= at's >>> "easy" with string diagrams but a lot of work to translate into formali= zed >>> 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=3DTSCggv_YE7M&t=3D4350= s): >>>> >>>> Given two higher paths p, q : 1_x =3D 1_x, Eckmann-Hilton gives us a p= ath >>>> EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p) =3D 1_{p@q=3Dq_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-051= 6-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/CAO0tDg7MCVQWLfSf1= 3PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >>> >>> . >>> >> --=20 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 e= mail 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. --000000000000c5e9c505bd068b15 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The generator of \pi_4(S^3) is the image of the generator= of \pi_3(S^2) under stabilization.=C2=A0 This is just the surjective the p= art of Freudenthal.=C2=A0 So to see that this generator has order dividing = 2 one needs exactly two things: the syllepsis, and my follow-up question ab= out EH giving the generator of \pi_3(S^2).=C2=A0 This is why I asked the fo= llow-up question.

Note t= hat 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 mathe= maticians via framed bordism theory (already Pontryagin knew these two fact= s almost a hundred years ago).=C2=A0 So informally it=E2=80=99s clear to ma= thematicians that the syllepsis shows this number is 1 or 2.=C2=A0 Formaliz= ing this well-known result remains an interesting question of course.
=

Best,
=
Noah=C2=A0


On M= on, 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 accura= te. 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 generat= es the group. There could be many elements of order 2.

=
Best wishes,
Egbert

On Mon, Mar 8, 2021 at 9:44 AM Egbe= rt Rijke <e.m.r= ijke@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 al= l the pseudocode already.

Best wishes,
E= gbert

On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
<= /div>
On the subject of formalization and = the syllepsis, has it ever been formalized that Eckman-Hilton gives the gen= erator of \pi_3(S^2)?=C2=A0 That is, we can build a 3-loop for S^2 by refl_= refl_base --> surf \circ surf^{-1} --EH--> surf^{-1} \circ surf -->= ; =C2=A0refl_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 (whi= ch 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=C2=A0a lot of associators = and other details.=C2=A0 One could also ask whether this generator is the s= ame as the one in my first paragraph.=C2=A0 This should be of comparable di= fficulty to the syllepsis (perhaps easier), but is another good example of = something that's "easy" with string diagrams but a lot of wor= k to translate into formalized HoTT.

Best,

Noah

On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojak= ova <so= jakova.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/w= atch?v=3DTSCggv_YE7M&t=3D4350s):

Given two higher paths p, q : 1_x =3D 1_x, Eckmann-Hilton gives us a path <= br> EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p) =3D 1_{p@q=3Dq_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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg= 7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com.

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