Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeDec 29th 2014
   • (edited Dec 29th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexat _[[Mayer-Vietoris sequence]]_ I had once recorded (previous nForum discussion is [here](http://nforum.mathforge.org/discussion/3418/mayervietoris-sequence/?Focus=28019#Comment_28019)) some observations about the generality in which Mayer-Vietoris-like homotopy fiber sequences exist in infinity-toposes. In the section _[Over an infinity-group](http://ncatlab.org/nlab/show/Mayer-Vietoris+sequence#OverAGroupObject)_ are discussed sufficient conditions such that for $f : X \to B$ and $g: Y \to B$ two morphisms in an $\infty$-topos to an object $B$ that carries $\infty$-group structure, we obtain a long homotopy fiber sequence of the form $$ \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?

   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 : X \to B$ and $g: Y \to B$ two morphisms in an $\infty$-topos to an object $B$ that carries $\infty$-group structure, we obtain a long homotopy fiber sequence of the form

   $$\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?

2. • CommentRowNumber2.
   • CommentAuthorMarc Hoyois
   • CommentTimeDec 29th 2014
   • PermaLink
   Author: Marc Hoyois
   Format: MarkdownItexCan't you just do everything pointwise? The assumption that $B \to B\times B\to B$ is a fiber sequence for $B$ an ∞-group holds in $\infty Grpd$, hence it should hold in any ∞-category $C$ which admits a finite-limit-preserving embedding in a presheaf ∞-category.

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

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeDec 30th 2014
   • (edited Dec 30th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOh, of course, thanks. That also answers my [other question](http://nforum.mathforge.org/discussion/6404/canonical-framing-of-differentially-cohesive-infinitygroups/#Item_1). 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorMarc Hoyois
   • CommentTimeDec 30th 2014
   • PermaLink
   Author: Marc Hoyois
   Format: MarkdownItexAh but the sequence $B \to B\times B\to B$ to be proved a fiber sequence is in fact equivalent to the trivial fiber sequence $$ B \xrightarrow{(id,e)} B \times B \xrightarrow{\pi_2} B, $$ by sending $(b_1,b_2)$ to $(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.

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

   $$B \xrightarrow{(id,e)} B \times B \xrightarrow{\pi_2} B,$$

   by sending $(b_1,b_2)$ to $(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.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeDec 30th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe only point to be proved is that $X\times_B Y$ is the fiber of $f \cdot g^{-1}$, right? That should be easy to do internally in HoTT.

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

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeDec 30th 2014
   • (edited Dec 30th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> The only point to be proved is that $X\times_B Y$ is the fiber of $f \cdot g^{-1}$, right? Yes, exactly. And the [other thing](http://nforum.mathforge.org/discussion/6404/canonical-framing-of-differentially-cohesive-infinitygroups/?Focus=51405#Comment_51405) that it would be nice to have internal proof of is that there is a homotopy pullback of the form $$ \array{ G \times D &\longrightarrow& D \\ \downarrow && \downarrow \\ G \times G &\stackrel{(-)\cdot (-)^{-1}}{\longrightarrow}& G } $$ for all $D\to G$. (This implies the first statement.)

   The only point to be proved is that $X\times_B Y$ is the fiber of $f \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

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

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

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 30th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhat is the map $G\times D \to G\times G$?

   What is the map $G\times D \to G\times G$?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeDec 30th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOh, I bet it is something like $(g,d) \mapsto (\phi(d)\cdot g,g)$, where $\phi: D\to G$. Right?

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

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 30th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHere's a HoTT proof of your second statement. $$ \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 $\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 $G$ to be a grouplike associative H-space, and since it doesn't use univalence it works in any lcc $(\infty,1)$-category.

   Here’s a HoTT proof of your second statement.

   $$\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 $\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 $G$ to be a grouplike associative H-space, and since it doesn’t use univalence it works in any lcc $(\infty,1)$-category.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> any ∞-category $C$ which admits a finite-limit-preserving embedding in a presheaf ∞-category. That would be *every* ∞-category, by the Yoneda embedding, right?

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

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

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Mike! Of course the key step is the first one $ 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 $sSet$ and then in $Set$, such as to then be able to appeal to this cancellation there. I trust that you easily deduce the term $cancelright$ for the case that $G \coloneqq (x = x)_X$?

    Thanks, Mike!

    Of course the key step is the first one

    $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 $sSet$ and then in $Set$, such as to then be able to appeal to this cancellation there.

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

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes. Concatenation with any path $p:y=z$ defines an equivalence $(x=y)\to (x=z)$, whose inverse is concatenation with $p^{-1}$. And the action of any equivalence on path-spaces is itself an equivalence. Combining those in the case $p=g_2$, we get an equivalence $(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_1 \cdot g_2^{-1})\cdot g_2$.

    Yes. Concatenation with any path $p:y=z$ defines an equivalence $(x=y)\to (x=z)$, whose inverse is concatenation with $p^{-1}$. And the action of any equivalence on path-spaces is itself an equivalence. Combining those in the case $p=g_2$, we get an equivalence $(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_1 \cdot g_2^{-1})\cdot g_2$.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexThank you. I see that this is basic stuff. Good. I have started to add some of this to [the section](http://ncatlab.org/nlab/show/Mayer-Vietoris%20sequence#OverAGroupObject) 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have fixed some formatting issues that I had left in [that section](http://ncatlab.org/nlab/show/Mayer-Vietoris%20sequence#OverAGroupObject) some cdots instead of cdot and a broken anchor link. Notice that none of the $(\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 $n$Lab 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.

    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 $(\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 $n$Lab 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.