Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2014
    • (edited Dec 29th 2014)

    at Mayer-Vietoris sequence I had once recorded (previous nForum discussion is here) some observations about the generality in which Mayer-Vietoris-like homotopy fiber sequences exist in infinity-toposes.

    In the section Over an infinity-group are discussed sufficient conditions such that for f:XBf : X \to B and g:YBg: Y \to B two morphisms in an \infty-topos to an object BB that carries \infty-group structure, we obtain a long homotopy fiber sequence of the form

    ΩBX× BYX×Yfg 1B \Omega B \longrightarrow X \times_B Y \longrightarrow X \times Y \stackrel{f \cdot g^{-1}}{\longrightarrow} B

    The discussion in Example 2 in that section in that entry gives this under the assumption that the \infty-topos is 1-localic, hence that it has a 1-site of definition. Or rather, in that case another discussion gives that every group object in the \infty-topos is presented by a presheaf of simplicial groups, and the discussion at Mayer-Vietoris sequence takes that to deduce the above fiber sequence.

    But all this smells like a hack for a statement that should be true more generally. In which generality do we have the above statement?

    • CommentRowNumber2.
    • CommentAuthorMarc Hoyois
    • CommentTimeDec 29th 2014

    Can’t you just do everything pointwise? The assumption that BB×BBB \to B\times B\to B is a fiber sequence for BB an ∞-group holds in Grpd\infty Grpd, hence it should hold in any ∞-category CC which admits a finite-limit-preserving embedding in a presheaf ∞-category.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014
    • (edited Dec 30th 2014)

    Oh, of course, thanks. That also answers my other question.

    On the other hand it would be nice to know how much one may say without making recourse to a site of definition, but just working internally.

    • CommentRowNumber4.
    • CommentAuthorMarc Hoyois
    • CommentTimeDec 30th 2014

    Ah but the sequence BB×BBB \to B\times B\to B to be proved a fiber sequence is in fact equivalent to the trivial fiber sequence

    B(id,e)B×Bπ 2B, B \xrightarrow{(id,e)} B \times B \xrightarrow{\pi_2} B,

    by sending (b 1,b 2)(b_1,b_2) to (b 1b 2 1,b 2)(b_1 b_2^{-1}, b_2) in the middle term. So you get this fiber sequence for any group object in any \infty-category.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    The only point to be proved is that X× BYX\times_B Y is the fiber of fg 1f \cdot g^{-1}, right? That should be easy to do internally in HoTT.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014
    • (edited Dec 30th 2014)

    The only point to be proved is that X× BYX\times_B Y is the fiber of fg 1f \cdot g^{-1}, right?

    Yes, exactly.

    And the other thing that it would be nice to have internal proof of is that there is a homotopy pullback of the form

    G×D D G×G ()() 1 G \array{ G \times D &\longrightarrow& D \\ \downarrow && \downarrow \\ G \times G &\stackrel{(-)\cdot (-)^{-1}}{\longrightarrow}& G }

    for all DGD\to G. (This implies the first statement.)

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    What is the map G×DG×GG\times D \to G\times G?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    Oh, I bet it is something like (g,d)(ϕ(d)g,g)(g,d) \mapsto (\phi(d)\cdot g,g), where ϕ:DG\phi: D\to G. Right?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    Here’s a HoTT proof of your second statement.

    D× G(G×G) = d:D g 1:G g 2:G(g 1g 2 1=ϕ(d)) = d:D g 1:G g 2:G(g 1=ϕ(d)g 2) = d:D g 2:G g 1:G(g 1=ϕ(d)g 2) = d:D g 2:G1 =D×G \begin{aligned} D\times_G (G\times G) &= \sum_{d:D} \sum_{g_1:G} \sum_{g_2:G} (g_1\cdot g_2^{-1} = \phi(d)) \\ &= \sum_{d:D} \sum_{g_1:G} \sum_{g_2:G} (g_1 = \phi(d)\cdot g_2) \\ &= \sum_{d:D} \sum_{g_2:G} \sum_{g_1:G} (g_1 = \phi(d)\cdot g_2) \\ &= \sum_{d:D} \sum_{g_2:G} \mathbf{1}\\ &= D\times G \end{aligned}

    The third-to-fourth line is because g 1:G(g 1=ϕ(d)g 2)\sum_{g_1:G} (g_1 = \phi(d)\cdot g_2) is a one-sided based path-space (called by some a “coconut” for obscure reasons), hence contractible.

    This proof only requires GG to be a grouplike associative H-space, and since it doesn’t use univalence it works in any lcc (,1)(\infty,1)-category.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    any ∞-category CC which admits a finite-limit-preserving embedding in a presheaf ∞-category.

    That would be every ∞-category, by the Yoneda embedding, right?

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014

    Thanks, Mike!

    Of course the key step is the first one

    d:D,g 1:G,g 2:Gcancelright:(g 1g 2 1=ϕ(d))=(g 1=ϕ(d)g 2) d:D, g_1:G, g_2:G \vdash cancelright \colon (g_1\cdot g_2^{-1} = \phi(d)) = (g_1 = \phi(d)\cdot g_2)

    In the external proofs that I had considered, all the work was in reducing the situation to the situation in sSetsSet and then in SetSet, such as to then be able to appeal to this cancellation there.

    I trust that you easily deduce the term cancelrightcancelright for the case that G(x=x) XG \coloneqq (x = x)_X?

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014

    Yes. Concatenation with any path p:y=zp:y=z defines an equivalence (x=y)(x=z)(x=y)\to (x=z), whose inverse is concatenation with p 1p^{-1}. And the action of any equivalence on path-spaces is itself an equivalence. Combining those in the case p=g 2p=g_2, we get an equivalence (g 1g 2 1=ϕ(d))((g 1g 2 1)g 2=ϕ(d)g 2)(g_1\cdot g_2^{-1} =\phi(d))\to ((g_1 \cdot g_2^{-1})\cdot g_2= \phi(d)\cdot g_2). Then we just concatenate on the left by the coherence path g 1=(g 1g 2 1)g 2g_1 = (g_1 \cdot g_2^{-1})\cdot g_2.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014

    Thank you. I see that this is basic stuff. Good.

    I have started to add some of this to the section in the entry, towards the end. But I don’t have much time at the moment and the whole section remains in a somewhat curious state for the time being.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2015

    I have fixed some formatting issues that I had left in that section

    some cdots instead of cdot and a broken anchor link. Notice that none of the (,1)(\infty,1)-entries work for pointing to anchors inside them via

     [text](name#anchor)
    

    because the parenthesis in the name confuse the parser (though if it were more clever it should be able to handle this…)

    At times I have for that reason made redirects that omit the “,1”. But this is not a robust solution in the long run, for in the far bright future that lies ahead, the nnLab will be full of articles on \infty-category theory in the genuine sense of (,)(\infty,\infty)-categories…

    So here I just made the page name without any parenthesis a redirect.