[HoTT] Syllepsis for syllepsis

[HoTT] Syllepsis for syllepsis

[Kristina Sojakova]

Dear all,

I proved the higher-dimensional version of syllepsis at

https://github.com/kristinas/HoTT/blob/syllepsis2/theories/Homotopy/syllepsis

if it is of interest.

I'll be happy to answer any questions.

Best,

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/5255bd6d-8b20-a4e5-bc6b-4f8418bc6700%40gmail.com.

Re: [HoTT] Syllepsis for syllepsis

[andrej.bauer]

Dear Kristina,

any chance you could spare a few words in English on the content of your formalization? Not everyone reads Coq code for breakfast.

Many thanks in advance!

Andrej

-- 
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/1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56%40andrej.com.

Re: [HoTT] Syllepsis for syllepsis

[Kristina Sojakova]

Dear Andrej,

Indeed, my message could have been more user-friendly. The file contains 
alternative proofs of Eckmann-Hilton and syllepsis, together with the 
proofs of the coherences described in Section 8 of

https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf

The last coherence outlined in the paper is what I referred to as 
"syllepsis for syllepsis".

Best,

Kristina

On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
> Dear Kristina,
>
> any chance you could spare a few words in English on the content of your formalization? Not everyone reads Coq code for breakfast.
>
> Many thanks in advance!
>
> Andrej
>

-- 
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/8e549102-49ca-407f-e95f-22d971f4b9fe%40gmail.com.

Re: [HoTT] Syllepsis for syllepsis

[David Roberts]

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

Dear Kristina,

Am I correct in assuming that the "syllepsis for syllepsis" is the equality
of (4) and (5) in your paper?

Is this related to the fact stable pi_2 is Z/2?

Best,

On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <
sojakova.kristina@gmail.com> wrote:

> Dear Andrej,
>
> Indeed, my message could have been more user-friendly. The file contains
> alternative proofs of Eckmann-Hilton and syllepsis, together with the
> proofs of the coherences described in Section 8 of
>
> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>
> The last coherence outlined in the paper is what I referred to as
> "syllepsis for syllepsis".
>
> Best,
>
> Kristina
>
> On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
> > Dear Kristina,
> >
> > any chance you could spare a few words in English on the content of your
> formalization? Not everyone reads Coq code for breakfast.
> >
> > Many thanks in advance!
> >
> > Andrej
> >
>
> --
> 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/8e549102-49ca-407f-e95f-22d971f4b9fe%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/CAFL%2BZM-%2Bkw%3D_VbtnLAkmdnEvmJSC8PCUf3NfK6hc%2ByYN_zuszQ%40mail.gmail.com.

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

Re: [HoTT] Syllepsis for syllepsis

[Kristina Sojakova]

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

Hello David,

On 7/8/2023 4:00 PM, David Roberts wrote:
> Dear Kristina,
>
> Am I correct in assuming that the "syllepsis for syllepsis" is the 
> equality of (4) and (5) in your paper?
Indeed, we show the equality between (4) and (5).
>
> Is this related to the fact stable pi_2 is Z/2?

We do not yet understand the implications of this result, that's another 
interesting question I guess. Do you have a conjecture here?

Kristina

>
> Best,
>
> On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, 
> <sojakova.kristina@gmail.com> wrote:
>
>     Dear Andrej,
>
>     Indeed, my message could have been more user-friendly. The file
>     contains
>     alternative proofs of Eckmann-Hilton and syllepsis, together with the
>     proofs of the coherences described in Section 8 of
>
>     https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>
>     The last coherence outlined in the paper is what I referred to as
>     "syllepsis for syllepsis".
>
>     Best,
>
>     Kristina
>
>     On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
>     > Dear Kristina,
>     >
>     > any chance you could spare a few words in English on the content
>     of your formalization? Not everyone reads Coq code for breakfast.
>     >
>     > Many thanks in advance!
>     >
>     > Andrej
>     >
>
>     -- 
>     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
>     <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
>     To view this discussion on the web visit
>     https://groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d971f4b9fe%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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com.

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

Re: [HoTT] Syllepsis for syllepsis

[Noah Snyder]

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

Very nice! I really like this line of research!

Let me try my hand at sketching what consequences I think this has for
homotopy groups of spheres. This isn't exactly my area of expertise so I
may have messed up something here. There's a TL;DR below.

As a warmup let's talk about Eckmann-Hilton itself. EH says that if x and y
are 2-loops, then xy = yx. Since this involves two variables this is a
statement about a homotopy group of a wedge of spheres S^2 wedge S^2,
namely it says that the commutator xyx^-1y^-1 which is non-trivial in
\pi_1(S^1 wedge S^1) becomes trivial when you suspend it to get an element
of \pi_2(S^2 wedge S^2). In other words, it gives a new relation
(commutativity) in \pi_2(S^2 wedge S^2). From this viewpoint we can also
easily get a statements about homotopy groups of wedges of spheres for more
elaborate constructions. In particular, the syllepsis says that a certain
element of \pi_3(S^2 wedge S^2) vanishes when you suspend it to \pi_4(S^3
wedge S^3). Finally, the "syllepsis of the syllepsis" (henceforth SoS,
though see the postscript) says that a certain element of pi_5(S^3 wedge
S^3) vanishes when you suspend it to pi_6(S^4 wedge S^4).

Ok, but people are usually more interested in homotopy groups of spheres,
rather than of wedges of two spheres. So let's go back to Eckmann-Hilton
and think some more. We can consider EH where both variables are the same
loop x (or, if you prefer, one is x and the other is x^-1) so that now
we're talking about homotopy groups of a single sphere. Here something
interesting happens, note that EH now gives an equality xx = xx, but we
already knew xx = xx! Indeed if you look at the suspension map \pi_1(S^1)
--> \pi_2 (S^2) it's an isomorphism, so we're not adding a new relation.
Instead we're saying that xx = xx in two different ways! First xx = xx via
refl but second xx = xx via EH. If we compose one of these trivializations
with the inverse of the other, what we end up with is a new element of
pi_3(S^2). This is how EH is related to pi_3(S^2).

Now let's think about what the syllepsis says about homotopy groups of
spheres. So now we again want to look at the syllepsis of x with itself.
This tells us that the element of pi_3(S^2) that we constructed from EH
composed with itself will become trivial when suspended into pi_4(S^3). In
this case this is killing 2 in Z, and so it really does add a new relation.

Ok, now let's turn to SoS, and again restrict our attention to SoS of x
with itself. This says that a certain element of pi_5(S^3) vanishes when
suspended to pi_6(S^4). But if you look at the homotopy groups the map
pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is analogous to
what happened for EH!), in particular the paths (4) and (5) from Kristina's
paper are already equal when p = q without assuming they're 4-loops! (I
haven't thought at all how one would go about proving this though!) So
instead we do what we did for EH, for a 4-loop x we have two different ways
of showing (4) = (5) and this gives us an interesting element of pi_7(S^4).
And looking in the table there is an interesting new element of pi_7(S^4)
that doesn't come from pi_6(S^3), and I'd guess this construction gives
this new generator of pi_7(S^4).

Remark: Note that in general there's not a 1-to-1 relationship between
interesting generators and relations in the homotopy groups of spheres
(which are operations of one variable!) and interesting operations of two
variables. You might need to write down a pretty elaborate composition of
operators in two variables to write down a generator or relation in
homotopy groups of spheres. In particular, the generator of pi_4(S^2) is a
more elaborate composition (it's essentially EH applied to EH), the
relation 2=0 in pi_4(S^2) is also more elaborate, and the generator of
pi_6(S^3) is much much more elaborate! (In particular, the generator of
pi_6(S^3) was essentially constructed by Andre Henriques, but in globular
instead of HoTT so it's missing all the unitors and associators. Even
without all the associators and unitors it's already extremely complicated!
See http://globular.science/1702.001v2)

TL;DR: First show that if you assume p = q then (4) = (5) is already true
for 3-loops. Then taking p to be a 4-loop compose the proof of (4) = (5)
using that p=q with the inverse of the syllepsis of the syllepsis and
you'll get an element of pi_7(S^4) which hopefully is the generator of the
copy of Z in Z x Z/12 = pi_7(S^4).

Best,

Noah

p.s. I wanted to push back a little on this "syllepsis of the syllepsis"
name. The "syllepsis" gets its name because it's what you need to turn a
"braided monoidal 2-category" into a "sylleptic monoidal 2-category."
(Sylleptic in turn is just "symmetric" but changing "m" to "l" to make it a
little bit less symmetric.) The "syllepsis of the syllepsis" by contrast is
what's needed to turn a "sylleptic monoidal 2-category" into a "symmetric
monoidal 2-category." That is, the parallel name would be the "symmetsis"
or something similar. Perhaps a better nomenclature would be to use the E1
= monoidal, E2 = braided monoidal, E3, etc. phrasing which isn't specific
to 2-categories. So you might call Eckman-Hilton the E2-axiom, the
syllepsis the E3-axiom, and the SoS the E4-axiom. There will also be an
E5-axiom, though because of stability you won't see that when studying
2-categories, it'll come up when you look at 3-categories. Another way you
might talk about it is the syllepsis is the "coherence of EH" while the
syllepsis of the syllepsis is "the coherence of the coherence of EH" which
I think maybe matches how you're thinking about the word sylleptsis?

On Sat, Jul 8, 2023 at 4:14 PM Kristina Sojakova <
sojakova.kristina@gmail.com> wrote:

> Hello David,
> On 7/8/2023 4:00 PM, David Roberts wrote:
>
> Dear Kristina,
>
> Am I correct in assuming that the "syllepsis for syllepsis" is the
> equality of (4) and (5) in your paper?
>
> Indeed, we show the equality between (4) and (5).
>
>
> Is this related to the fact stable pi_2 is Z/2?
>
> We do not yet understand the implications of this result, that's another
> interesting question I guess. Do you have a conjecture here?
>
> Kristina
>
>
> Best,
>
> On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <
> sojakova.kristina@gmail.com> wrote:
>
>> Dear Andrej,
>>
>> Indeed, my message could have been more user-friendly. The file contains
>> alternative proofs of Eckmann-Hilton and syllepsis, together with the
>> proofs of the coherences described in Section 8 of
>>
>> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>>
>> The last coherence outlined in the paper is what I referred to as
>> "syllepsis for syllepsis".
>>
>> Best,
>>
>> Kristina
>>
>> On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
>> > Dear Kristina,
>> >
>> > any chance you could spare a few words in English on the content of
>> your formalization? Not everyone reads Coq code for breakfast.
>> >
>> > Many thanks in advance!
>> >
>> > Andrej
>> >
>>
>> --
>> 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/8e549102-49ca-407f-e95f-22d971f4b9fe%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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.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/CAO0tDg60ZcCDTgXM7WSWv7uQjCR5nmLe04X2y24uPge5HK%2B39w%40mail.gmail.com.

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

Re: [HoTT] Syllepsis for syllepsis

[Kristina Sojakova]

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

Thanks for all this Noah! Not being an expert, I will need some time to 
digest all the details, but my first question is this: I proved the 
equality of (4) and (5) for 4-loops p, q. Do we expect this should hold 
at a lower dimension too?

On 7/10/2023 7:43 PM, Noah Snyder wrote:
> Very nice! I really like this line of research!
>
> Let me try my hand at sketching what consequences I think this has for 
> homotopy groups of spheres. This isn't exactly my area of expertise so 
> I may have messed up something here. There's a TL;DR below.
>
> As a warmup let's talk about Eckmann-Hilton itself. EH says that if x 
> and y are 2-loops, then xy = yx. Since this involves two variables 
> this is a statement about a homotopy group of a wedge of spheres S^2 
> wedge S^2, namely it says that the commutator xyx^-1y^-1 which is 
> non-trivial in \pi_1(S^1 wedge S^1) becomes trivial when you suspend 
> it to get an element of \pi_2(S^2 wedge S^2). In other words, it gives 
> a new relation (commutativity) in \pi_2(S^2 wedge S^2). From this 
> viewpoint we can also easily get a statements about homotopy groups of 
> wedges of spheres for more elaborate constructions. In particular, the 
> syllepsis says that a certain element of \pi_3(S^2 wedge S^2) vanishes 
> when you suspend it to \pi_4(S^3 wedge S^3). Finally, the "syllepsis 
> of the syllepsis" (henceforth SoS, though see the postscript) says 
> that a certain element of pi_5(S^3 wedge S^3) vanishes when you 
> suspend it to pi_6(S^4 wedge S^4).
>
> Ok, but people are usually more interested in homotopy groups of 
> spheres, rather than of wedges of two spheres. So let's go back to 
> Eckmann-Hilton and think some more. We can consider EH where both 
> variables are the same loop x (or, if you prefer, one is x and the 
> other is x^-1) so that now we're talking about homotopy groups of a 
> single sphere. Here something interesting happens, note that EH now 
> gives an equality xx = xx, but we already knew xx = xx! Indeed if you 
> look at the suspension map \pi_1(S^1) --> \pi_2 (S^2) it's an 
> isomorphism, so we're not adding a new relation. Instead we're saying 
> that xx = xx in two different ways! First xx = xx via refl but second 
> xx = xx via EH. If we compose one of these trivializations with the 
> inverse of the other, what we end up with is a new element of 
> pi_3(S^2). This is how EH is related to pi_3(S^2).
>
> Now let's think about what the syllepsis says about homotopy groups of 
> spheres. So now we again want to look at the syllepsis of x with 
> itself. This tells us that the element of pi_3(S^2) that we 
> constructed from EH composed with itself will become trivial when 
> suspended into pi_4(S^3). In this case this is killing 2 in Z, and so 
> it really does add a new relation.
>
> Ok, now let's turn to SoS, and again restrict our attention to SoS of 
> x with itself. This says that a certain element of pi_5(S^3) vanishes 
> when suspended to pi_6(S^4). But if you look at the homotopy groups 
> the map pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is 
> analogous to what happened for EH!), in particular the paths (4) and 
> (5) from Kristina's paper are already equal when p = q without 
> assuming they're 4-loops! (I haven't thought at all how one would go 
> about proving this though!) So instead we do what we did for EH, for a 
> 4-loop x we have two different ways of showing (4) = (5) and this 
> gives us an interesting element of pi_7(S^4). And looking in the table 
> there is an interesting new element of pi_7(S^4) that doesn't come 
> from pi_6(S^3), and I'd guess this construction gives this new 
> generator of pi_7(S^4).
>
> Remark: Note that in general there's not a 1-to-1 relationship between 
> interesting generators and relations in the homotopy groups of spheres 
> (which are operations of one variable!) and interesting operations of 
> two variables. You might need to write down a pretty elaborate 
> composition of operators in two variables to write down a generator or 
> relation in homotopy groups of spheres. In particular, the generator 
> of pi_4(S^2) is a more elaborate composition (it's essentially EH 
> applied to EH), the relation 2=0 in pi_4(S^2) is also more elaborate, 
> and the generator of pi_6(S^3) is much much more elaborate! (In 
> particular, the generator of pi_6(S^3) was essentially constructed by 
> Andre Henriques, but in globular instead of HoTT so it's missing all 
> the unitors and associators. Even without all the associators and 
> unitors it's already extremely complicated! See 
> http://globular.science/1702.001v2)
>
> TL;DR: First show that if you assume p = q then (4) = (5) is already 
> true for 3-loops. Then taking p to be a 4-loop compose the proof of 
> (4) = (5) using that p=q with the inverse of the syllepsis of the 
> syllepsis and you'll get an element of pi_7(S^4) which hopefully is 
> the generator of the copy of Z in Z x Z/12 = pi_7(S^4).
>
> Best,
>
> Noah
>
> p.s. I wanted to push back a little on this "syllepsis of the 
> syllepsis" name. The "syllepsis" gets its name because it's what you 
> need to turn a "braided monoidal 2-category" into a "sylleptic 
> monoidal 2-category." (Sylleptic in turn is just "symmetric" but 
> changing "m" to "l" to make it a little bit less symmetric.) The 
> "syllepsis of the syllepsis" by contrast is what's needed to turn a 
> "sylleptic monoidal 2-category" into a "symmetric monoidal 
> 2-category." That is, the parallel name would be the "symmetsis" or 
> something similar. Perhaps a better nomenclature would be to use the 
> E1 = monoidal, E2 = braided monoidal, E3, etc. phrasing which isn't 
> specific to 2-categories. So you might call Eckman-Hilton the 
> E2-axiom, the syllepsis the E3-axiom, and the SoS the E4-axiom. There 
> will also be an E5-axiom, though because of stability you won't see 
> that when studying 2-categories, it'll come up when you look at 
> 3-categories. Another way you might talk about it is the syllepsis is 
> the "coherence of EH" while the syllepsis of the syllepsis is "the 
> coherence of the coherence of EH" which I think maybe matches how 
> you're thinking about the word sylleptsis?
>
> On Sat, Jul 8, 2023 at 4:14 PM Kristina Sojakova 
> <sojakova.kristina@gmail.com> wrote:
>
>     Hello David,
>
>     On 7/8/2023 4:00 PM, David Roberts wrote:
>>     Dear Kristina,
>>
>>     Am I correct in assuming that the "syllepsis for syllepsis" is
>>     the equality of (4) and (5) in your paper?
>     Indeed, we show the equality between (4) and (5).
>>
>>     Is this related to the fact stable pi_2 is Z/2?
>
>     We do not yet understand the implications of this result, that's
>     another interesting question I guess. Do you have a conjecture here?
>
>     Kristina
>
>>
>>     Best,
>>
>>     On Sat, 8 July 2023, 10:46 pm Kristina Sojakova,
>>     <sojakova.kristina@gmail.com> wrote:
>>
>>         Dear Andrej,
>>
>>         Indeed, my message could have been more user-friendly. The
>>         file contains
>>         alternative proofs of Eckmann-Hilton and syllepsis, together
>>         with the
>>         proofs of the coherences described in Section 8 of
>>
>>         https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>>
>>         The last coherence outlined in the paper is what I referred
>>         to as
>>         "syllepsis for syllepsis".
>>
>>         Best,
>>
>>         Kristina
>>
>>         On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
>>         > Dear Kristina,
>>         >
>>         > any chance you could spare a few words in English on the
>>         content of your formalization? Not everyone reads Coq code
>>         for breakfast.
>>         >
>>         > Many thanks in advance!
>>         >
>>         > Andrej
>>         >
>>
>>         -- 
>>         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
>>         <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
>>         To view this discussion on the web visit
>>         https://groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d971f4b9fe%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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com
>     <https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.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/d5413565-49e2-6293-0b90-72003a3b1ab3%40gmail.com.

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

Re: [HoTT] Syllepsis for syllepsis

[Noah Snyder]

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

For general p and q you need to assume that they're 4-loops, but if p=q
then it should hold for 3-loops! Analogously xx = xx for 1-loops, but xy =
yx only for 2-loops. Best,

Noah

On Mon, Jul 10, 2023 at 2:46 PM Kristina Sojakova <
sojakova.kristina@gmail.com> wrote:

> Thanks for all this Noah! Not being an expert, I will need some time to
> digest all the details, but my first question is this: I proved the
> equality of (4) and (5) for 4-loops p, q. Do we expect this should hold at
> a lower dimension too?
> On 7/10/2023 7:43 PM, Noah Snyder wrote:
>
> Very nice! I really like this line of research!
>
> Let me try my hand at sketching what consequences I think this has for
> homotopy groups of spheres. This isn't exactly my area of expertise so I
> may have messed up something here. There's a TL;DR below.
>
> As a warmup let's talk about Eckmann-Hilton itself. EH says that if x and
> y are 2-loops, then xy = yx. Since this involves two variables this is a
> statement about a homotopy group of a wedge of spheres S^2 wedge S^2,
> namely it says that the commutator xyx^-1y^-1 which is non-trivial in
> \pi_1(S^1 wedge S^1) becomes trivial when you suspend it to get an element
> of \pi_2(S^2 wedge S^2). In other words, it gives a new relation
> (commutativity) in \pi_2(S^2 wedge S^2). From this viewpoint we can also
> easily get a statements about homotopy groups of wedges of spheres for more
> elaborate constructions. In particular, the syllepsis says that a certain
> element of \pi_3(S^2 wedge S^2) vanishes when you suspend it to \pi_4(S^3
> wedge S^3). Finally, the "syllepsis of the syllepsis" (henceforth SoS,
> though see the postscript) says that a certain element of pi_5(S^3 wedge
> S^3) vanishes when you suspend it to pi_6(S^4 wedge S^4).
>
> Ok, but people are usually more interested in homotopy groups of spheres,
> rather than of wedges of two spheres. So let's go back to Eckmann-Hilton
> and think some more. We can consider EH where both variables are the same
> loop x (or, if you prefer, one is x and the other is x^-1) so that now
> we're talking about homotopy groups of a single sphere. Here something
> interesting happens, note that EH now gives an equality xx = xx, but we
> already knew xx = xx! Indeed if you look at the suspension map \pi_1(S^1)
> --> \pi_2 (S^2) it's an isomorphism, so we're not adding a new relation.
> Instead we're saying that xx = xx in two different ways! First xx = xx via
> refl but second xx = xx via EH. If we compose one of these trivializations
> with the inverse of the other, what we end up with is a new element of
> pi_3(S^2). This is how EH is related to pi_3(S^2).
>
> Now let's think about what the syllepsis says about homotopy groups of
> spheres. So now we again want to look at the syllepsis of x with itself.
> This tells us that the element of pi_3(S^2) that we constructed from EH
> composed with itself will become trivial when suspended into pi_4(S^3). In
> this case this is killing 2 in Z, and so it really does add a new relation.
>
> Ok, now let's turn to SoS, and again restrict our attention to SoS of x
> with itself. This says that a certain element of pi_5(S^3) vanishes when
> suspended to pi_6(S^4). But if you look at the homotopy groups the map
> pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is analogous to
> what happened for EH!), in particular the paths (4) and (5) from Kristina's
> paper are already equal when p = q without assuming they're 4-loops! (I
> haven't thought at all how one would go about proving this though!) So
> instead we do what we did for EH, for a 4-loop x we have two different ways
> of showing (4) = (5) and this gives us an interesting element of pi_7(S^4).
> And looking in the table there is an interesting new element of pi_7(S^4)
> that doesn't come from pi_6(S^3), and I'd guess this construction gives
> this new generator of pi_7(S^4).
>
> Remark: Note that in general there's not a 1-to-1 relationship between
> interesting generators and relations in the homotopy groups of spheres
> (which are operations of one variable!) and interesting operations of two
> variables. You might need to write down a pretty elaborate composition of
> operators in two variables to write down a generator or relation in
> homotopy groups of spheres. In particular, the generator of pi_4(S^2) is a
> more elaborate composition (it's essentially EH applied to EH), the
> relation 2=0 in pi_4(S^2) is also more elaborate, and the generator of
> pi_6(S^3) is much much more elaborate! (In particular, the generator of
> pi_6(S^3) was essentially constructed by Andre Henriques, but in globular
> instead of HoTT so it's missing all the unitors and associators. Even
> without all the associators and unitors it's already extremely complicated!
> See http://globular.science/1702.001v2)
>
> TL;DR: First show that if you assume p = q then (4) = (5) is already true
> for 3-loops. Then taking p to be a 4-loop compose the proof of (4) = (5)
> using that p=q with the inverse of the syllepsis of the syllepsis and
> you'll get an element of pi_7(S^4) which hopefully is the generator of the
> copy of Z in Z x Z/12 = pi_7(S^4).
>
> Best,
>
> Noah
>
> p.s. I wanted to push back a little on this "syllepsis of the syllepsis"
> name. The "syllepsis" gets its name because it's what you need to turn a
> "braided monoidal 2-category" into a "sylleptic monoidal 2-category."
> (Sylleptic in turn is just "symmetric" but changing "m" to "l" to make it a
> little bit less symmetric.) The "syllepsis of the syllepsis" by contrast is
> what's needed to turn a "sylleptic monoidal 2-category" into a "symmetric
> monoidal 2-category." That is, the parallel name would be the "symmetsis"
> or something similar. Perhaps a better nomenclature would be to use the E1
> = monoidal, E2 = braided monoidal, E3, etc. phrasing which isn't specific
> to 2-categories. So you might call Eckman-Hilton the E2-axiom, the
> syllepsis the E3-axiom, and the SoS the E4-axiom. There will also be an
> E5-axiom, though because of stability you won't see that when studying
> 2-categories, it'll come up when you look at 3-categories. Another way you
> might talk about it is the syllepsis is the "coherence of EH" while the
> syllepsis of the syllepsis is "the coherence of the coherence of EH" which
> I think maybe matches how you're thinking about the word sylleptsis?
>
> On Sat, Jul 8, 2023 at 4:14 PM Kristina Sojakova <
> sojakova.kristina@gmail.com> wrote:
>
>> Hello David,
>> On 7/8/2023 4:00 PM, David Roberts wrote:
>>
>> Dear Kristina,
>>
>> Am I correct in assuming that the "syllepsis for syllepsis" is the
>> equality of (4) and (5) in your paper?
>>
>> Indeed, we show the equality between (4) and (5).
>>
>>
>> Is this related to the fact stable pi_2 is Z/2?
>>
>> We do not yet understand the implications of this result, that's another
>> interesting question I guess. Do you have a conjecture here?
>>
>> Kristina
>>
>>
>> Best,
>>
>> On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <
>> sojakova.kristina@gmail.com> wrote:
>>
>>> Dear Andrej,
>>>
>>> Indeed, my message could have been more user-friendly. The file contains
>>> alternative proofs of Eckmann-Hilton and syllepsis, together with the
>>> proofs of the coherences described in Section 8 of
>>>
>>> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>>>
>>> The last coherence outlined in the paper is what I referred to as
>>> "syllepsis for syllepsis".
>>>
>>> Best,
>>>
>>> Kristina
>>>
>>> On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
>>> > Dear Kristina,
>>> >
>>> > any chance you could spare a few words in English on the content of
>>> your formalization? Not everyone reads Coq code for breakfast.
>>> >
>>> > Many thanks in advance!
>>> >
>>> > Andrej
>>> >
>>>
>>> --
>>> 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/8e549102-49ca-407f-e95f-22d971f4b9fe%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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.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/CAO0tDg4PM3dvNSOEXHo3YTYFku5zR6tRP5W9zeEn_F4A8UGaww%40mail.gmail.com.

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

Re: [HoTT] Syllepsis for syllepsis

[Raymond Baker]

[-- Attachment #1.1: Type: text/plain, Size: 10338 bytes --]

I stumbled upon this thread a (quite bit) late, so sorry for chiming in out 
of the blue. But I have a way of showing that EH(x,x) gets you a generator 
of pi3(S2) in HoTT. I a gave a short talk about it at CMU's HoTT2023, and 
should soon be submitting a revised write up to the special issue in MSCS. 

Its quite cool to see the construction of the expected generator of 
pi7(S4). It makes me wonder how much one could adapt what goes on in the EH 
and Hopf proof for these higher dimensions.

Related, I think all thats missing from Noah's message that is required to 
compute pi4(S3) is a non-triviality proof. Is there a good reference for 
this in book HoTT?
On Monday, July 10, 2023 at 12:49:33 PM UTC-6 Noah Snyder wrote:

> For general p and q you need to assume that they're 4-loops, but if p=q 
> then it should hold for 3-loops! Analogously xx = xx for 1-loops, but xy = 
> yx only for 2-loops. Best,
>
> Noah
>
> On Mon, Jul 10, 2023 at 2:46 PM Kristina Sojakova <sojakova...@gmail.com> 
> wrote:
>
>> Thanks for all this Noah! Not being an expert, I will need some time to 
>> digest all the details, but my first question is this: I proved the 
>> equality of (4) and (5) for 4-loops p, q. Do we expect this should hold at 
>> a lower dimension too?
>> On 7/10/2023 7:43 PM, Noah Snyder wrote:
>>
>> Very nice! I really like this line of research!
>>
>> Let me try my hand at sketching what consequences I think this has for 
>> homotopy groups of spheres. This isn't exactly my area of expertise so I 
>> may have messed up something here. There's a TL;DR below.
>>
>> As a warmup let's talk about Eckmann-Hilton itself. EH says that if x and 
>> y are 2-loops, then xy = yx. Since this involves two variables this is a 
>> statement about a homotopy group of a wedge of spheres S^2 wedge S^2, 
>> namely it says that the commutator xyx^-1y^-1 which is non-trivial in 
>> \pi_1(S^1 wedge S^1) becomes trivial when you suspend it to get an element 
>> of \pi_2(S^2 wedge S^2). In other words, it gives a new relation 
>> (commutativity) in \pi_2(S^2 wedge S^2). From this viewpoint we can also 
>> easily get a statements about homotopy groups of wedges of spheres for more 
>> elaborate constructions. In particular, the syllepsis says that a certain 
>> element of \pi_3(S^2 wedge S^2) vanishes when you suspend it to \pi_4(S^3 
>> wedge S^3). Finally, the "syllepsis of the syllepsis" (henceforth SoS, 
>> though see the postscript) says that a certain element of pi_5(S^3 wedge 
>> S^3) vanishes when you suspend it to pi_6(S^4 wedge S^4).
>>
>> Ok, but people are usually more interested in homotopy groups of spheres, 
>> rather than of wedges of two spheres. So let's go back to Eckmann-Hilton 
>> and think some more. We can consider EH where both variables are the same 
>> loop x (or, if you prefer, one is x and the other is x^-1) so that now 
>> we're talking about homotopy groups of a single sphere. Here something 
>> interesting happens, note that EH now gives an equality xx = xx, but we 
>> already knew xx = xx! Indeed if you look at the suspension map \pi_1(S^1) 
>> --> \pi_2 (S^2) it's an isomorphism, so we're not adding a new relation. 
>> Instead we're saying that xx = xx in two different ways! First xx = xx via 
>> refl but second xx = xx via EH. If we compose one of these trivializations 
>> with the inverse of the other, what we end up with is a new element of 
>> pi_3(S^2). This is how EH is related to pi_3(S^2).
>>
>> Now let's think about what the syllepsis says about homotopy groups of 
>> spheres. So now we again want to look at the syllepsis of x with itself. 
>> This tells us that the element of pi_3(S^2) that we constructed from EH 
>> composed with itself will become trivial when suspended into pi_4(S^3). In 
>> this case this is killing 2 in Z, and so it really does add a new relation.
>>
>> Ok, now let's turn to SoS, and again restrict our attention to SoS of x 
>> with itself. This says that a certain element of pi_5(S^3) vanishes when 
>> suspended to pi_6(S^4). But if you look at the homotopy groups the map 
>> pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is analogous to 
>> what happened for EH!), in particular the paths (4) and (5) from Kristina's 
>> paper are already equal when p = q without assuming they're 4-loops! (I 
>> haven't thought at all how one would go about proving this though!) So 
>> instead we do what we did for EH, for a 4-loop x we have two different ways 
>> of showing (4) = (5) and this gives us an interesting element of pi_7(S^4). 
>> And looking in the table there is an interesting new element of pi_7(S^4) 
>> that doesn't come from pi_6(S^3), and I'd guess this construction gives 
>> this new generator of pi_7(S^4).
>>
>> Remark: Note that in general there's not a 1-to-1 relationship between 
>> interesting generators and relations in the homotopy groups of spheres 
>> (which are operations of one variable!) and interesting operations of two 
>> variables. You might need to write down a pretty elaborate composition of 
>> operators in two variables to write down a generator or relation in 
>> homotopy groups of spheres. In particular, the generator of pi_4(S^2) is a 
>> more elaborate composition (it's essentially EH applied to EH), the 
>> relation 2=0 in pi_4(S^2) is also more elaborate, and the generator of 
>> pi_6(S^3) is much much more elaborate! (In particular, the generator of 
>> pi_6(S^3) was essentially constructed by Andre Henriques, but in globular 
>> instead of HoTT so it's missing all the unitors and associators. Even 
>> without all the associators and unitors it's already extremely complicated! 
>> See http://globular.science/1702.001v2) 
>>
>> TL;DR: First show that if you assume p = q then (4) = (5) is already true 
>> for 3-loops. Then taking p to be a 4-loop compose the proof of (4) = (5) 
>> using that p=q with the inverse of the syllepsis of the syllepsis and 
>> you'll get an element of pi_7(S^4) which hopefully is the generator of the 
>> copy of Z in Z x Z/12 = pi_7(S^4).
>>
>> Best,
>>
>> Noah
>>
>> p.s. I wanted to push back a little on this "syllepsis of the syllepsis" 
>> name. The "syllepsis" gets its name because it's what you need to turn a 
>> "braided monoidal 2-category" into a "sylleptic monoidal 2-category." 
>> (Sylleptic in turn is just "symmetric" but changing "m" to "l" to make it a 
>> little bit less symmetric.) The "syllepsis of the syllepsis" by contrast is 
>> what's needed to turn a "sylleptic monoidal 2-category" into a "symmetric 
>> monoidal 2-category." That is, the parallel name would be the "symmetsis" 
>> or something similar. Perhaps a better nomenclature would be to use the E1 
>> = monoidal, E2 = braided monoidal, E3, etc. phrasing which isn't specific 
>> to 2-categories. So you might call Eckman-Hilton the E2-axiom, the 
>> syllepsis the E3-axiom, and the SoS the E4-axiom. There will also be an 
>> E5-axiom, though because of stability you won't see that when studying 
>> 2-categories, it'll come up when you look at 3-categories. Another way you 
>> might talk about it is the syllepsis is the "coherence of EH" while the 
>> syllepsis of the syllepsis is "the coherence of the coherence of EH" which 
>> I think maybe matches how you're thinking about the word sylleptsis?
>>
>> On Sat, Jul 8, 2023 at 4:14 PM Kristina Sojakova <sojakova...@gmail.com> 
>> wrote:
>>
>>> Hello David,
>>> On 7/8/2023 4:00 PM, David Roberts wrote:
>>>
>>> Dear Kristina, 
>>>
>>> Am I correct in assuming that the "syllepsis for syllepsis" is the 
>>> equality of (4) and (5) in your paper? 
>>>
>>> Indeed, we show the equality between (4) and (5). 
>>>
>>>
>>> Is this related to the fact stable pi_2 is Z/2?
>>>
>>> We do not yet understand the implications of this result, that's another 
>>> interesting question I guess. Do you have a conjecture here?
>>>
>>> Kristina
>>>
>>>
>>> Best,
>>>
>>> On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <sojakova...@gmail.com> 
>>> wrote:
>>>
>>>> Dear Andrej,
>>>>
>>>> Indeed, my message could have been more user-friendly. The file 
>>>> contains 
>>>> alternative proofs of Eckmann-Hilton and syllepsis, together with the 
>>>> proofs of the coherences described in Section 8 of
>>>>
>>>> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>>>>
>>>> The last coherence outlined in the paper is what I referred to as 
>>>> "syllepsis for syllepsis".
>>>>
>>>> Best,
>>>>
>>>> Kristina
>>>>
>>>> On 7/8/2023 2:22 PM, andrej...@andrej.com wrote:
>>>> > Dear Kristina,
>>>> >
>>>> > any chance you could spare a few words in English on the content of 
>>>> your formalization? Not everyone reads Coq code for breakfast.
>>>> >
>>>> > Many thanks in advance!
>>>> >
>>>> > Andrej
>>>> >
>>>>
>>>> -- 
>>>> 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 HomotopyTypeThe...@googlegroups.com.
>>>> To view this discussion on the web visit 
>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d971f4b9fe%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 HomotopyTypeThe...@googlegroups.com.
>>> To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com 
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.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/44399e68-2981-4ff6-8787-4da7c347b2c4n%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 16049 bytes --]