Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 14 of 14
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?
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.
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.
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.
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.
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.)
What is the map $G\times D \to G\times G$?
Oh, I bet it is something like $(g,d) \mapsto (\phi(d)\cdot g,g)$, where $\phi: D\to G$. Right?
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.
any ∞-category $C$ which admits a finite-limit-preserving embedding in a presheaf ∞-category.
That would be every ∞-category, by the Yoneda embedding, right?
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$?
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$.
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.
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.
1 to 14 of 14