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.
(…)
I had said something wrong there, then removed it.
So let me turn it into a question, instead: what can we say about how n-images behave under forming homotopy fibers?
If
$\array{ A &\stackrel{f}{\to}& B \\ \downarrow^{\mathrlap{h}} &\swArrow_\alpha& \downarrow^{\mathrlap{k}} \\ C &\stackrel{g}{\to}& D }$is a diagram in an $\infty$-topos with a compatible global point in $B$ and $D$, we get a induced objects
$fib(im_n(h) \to im_n(k))$and
$im_n(fib(f) \to fib(g))$with a map from the latter to the former. How far is that from being an equivalence?
Well, it appears to be an equivalence when $n=1$ and $n=\infty$…
I just came here to ask a question, only to notice that the question is still the one that I asked in #2 above. This must have a super-simple answer in HoTT. No?
Let’s see, probably some messing around with sigma-types will reduce it to the case when $C=D=1$. In that case the naive question becomes “does $n$-truncation preserve homotopy fibers?” And the answer to that is certainly no, e.g. if $A=1$ as well then you’re comparing the $n$-truncation of the loop space with the loop space of the $n$-truncation, which are of course not the same — the latter is the further $(n-1)$-truncation of the former. But since you actually asked “how far is that from being an equivalence?”, maybe we can say something about the connectivity and/or truncatedness of the connecting map; let me cogitate further.
Right, thanks, I should specify to some special case. It would seem to help me a lot if I knew conditions that gave an equivalence here under the assumption that $h$ and $k$ are the unit maps of a sharp modality, and that the square is the naturality square of the sharp modality on the top morphism. Not sure if this extra condition is of any help, though…
I think I see how to prove in general that the comparison map is $(n-1)$-connected. Since it’s automatically $n$-truncated (being a map between $n$-truncated objects), its failure to be an equivalence is measured by one homotopy group (or more precisely, in the non-connected case, one family of homotopy groups).
I don’t see immediately any way that bringing in a sharp modality helps.
Ah, thanks, excellent! That might just be sufficient for what I am looking at. (Will need to think later when I am not in a rush as now).
I could just as well say it: There is a canonical $Aut(\Sigma)$-action on $[\Sigma,\mathbf{B}^n \mathbb{G}_{conn}]$ and I want to see that this action passes to the “differential concretification” of this object as given by this formula, which is an iterated fiber product of $n$-images of the sharp unit.
Need to dash off now…
If it does turn out to be enough for what you need, let me know and I’ll go check the details of the argument I had in my head. (-:
Okay, now I am back. So it might just be enough, allow me think out loudly:
I’ll write $\sharp_n$ for the $n$-truncation of the unit of the sharp modality.
Given an action of $G$ on $V$ exhibited by a fiber sequence
$V \to V/G \to \mathbf{B}G$
I’d like to have an action of $\sharp_n G$ on $\sharp_n V$. So I hit the fiber sequence with $\sharp_{n+1}$ to get two consecutive maps
$\sharp_{n+1}V\to \sharp_{n+1}(V/G) \to \mathbf{B} \sharp_n G$
and from what you say this almost exhibits $\sharp_{n+1}V$ as the homotopy fiber, except for the topmost relative homotopy group.
Which might just be good, since I am expecting an action on $\sharp_n V$ instead, anyway, not on $\sharp_{n+1}V$. So maybe one may just further truncate on the left to get this?
I should say why I am expecting what I say I am expecting in #10, lest I am chasing us after the wrong goose again.
So from looking at this non-elementarily, i.e. allowing myself to use simplicial objects, then $V/G$ is the homotopy colimit of the simplicial object $(V/G)_\bullet = G^{\times_\bullet} \times V$.
Now I am thinking: $\sharp_n$ preserves products. Because $n$-image factorization satisfies $\im_n (X_1 \times Y_1 \stackrel{(f,g)}{\longrightarrow} X_2 \times Y_2) \simeq (\im_n(f) \times \im_n(g) \stackrel{}{\longrightarrow} X_2 \times Y_2)$. Because $n$-truncation preserves products and because we may write $(f,g)$ as a product of $(f,id)$ with $(id,g)$ in the slice over $X_2 \times Y_2$.
So that makes me think that from the simplicial object $(V/G)_\bullet$ I get a simplicial object $(\sharp_n(V)/\sharp_n(G))_\bullet = (\sharp_n G)^{\times_\bullet}\times \sharp_n V$. And this finally exhibits an induced action of $\sharp_n G$ on $\sharp_n V$.
Does that seem right?
So in the special case of looping of a morphism $f \colon X \to Y$ of pointed objects, we have a diagram of the form
$\array{ \Omega f \colon & \Omega X &\longrightarrow& im_n(\Omega f) &\longrightarrow& \Omega Y \\ & \downarrow && \downarrow && \downarrow \\ id_\ast \colon & \ast &\longrightarrow & im_{n+1}(id_\ast) \simeq \ast &\longrightarrow& \ast \\ & \downarrow && \downarrow && \downarrow \\ f\colon & X &\stackrel{}{\longrightarrow}& im_{n+1}(f) &\stackrel{}{\longrightarrow}& Y }$with the columns being homotopy fiber sequence. Do we have conditions such that more generally this becomes
$\array{ & fib(\alpha) &\longrightarrow& im_n(fib(\phi)) &\longrightarrow& fib(\beta) \\ & \downarrow && \downarrow && \downarrow \\ g \colon & X_1 &\longrightarrow & im_{n+1}(g) &\longrightarrow& Y_1 \\ & \downarrow^{\mathrlap{\alpha}} && \downarrow^{\mathrlap{\phi}} && \downarrow^{\mathrlap{\beta}} \\ f\colon & X_2 &\stackrel{}{\longrightarrow}& im_{n+1}(f) &\stackrel{}{\longrightarrow}& Y_2 }$?
Why is the middle column a fiber sequence in the case of looping?
I have sent you an email on this.
Hmm, so the second diagram in #12 cannot have the middle be a fiber sequence always. For instance, at the other extreme, if $X_2 = Y_2 = \ast$, then $fib(\alpha)=X_1$ and $fib(\beta) = Y_1$ and $fib(\phi) = g$, but the $n$-image and the $(n+1)$-image of $g$ are not the same. Of course in that case one has instead a fiber sequence with $im_{n+1}(fib(\phi))$ at the top.
But #11 does sound plausible. Is $\sharp_n$ by any chance a modality in its own right?
Here’s a HoTTer way to make $\sharp_n G$ act on $\sharp_n V$. Let $A:B\to Type$ be any type family; I claim there is an induced family $A^{\sharp_n} : \sharp_{n+1} B \to Type$ such that $A^{\sharp_n}(\eta_{n+1}(b)) = \sharp_n (A(b))$ for any $b:B$, where $\eta_{n+1} : B \to \sharp_{n+1} B$ is the inclusion. Applying this when $b$ is the basepoint of $\mathbf{B}G$ should give the desired action on the desired type.
First of all, we have the composite $B \xrightarrow{A} Type \xrightarrow{\sharp} Type_{\sharp}$, where $Type_{\sharp} = \sum_{X:Type} is\sharp(X)$. Since $Type_{\sharp}$ is itself $\sharp$ (since $\sharp$ is lex), this factors through $\sharp B$, giving a type family $A^\sharp : \sharp B \to Type_{\sharp}$ such that $A^{\sharp}(\eta(b)) = \sharp (A(b))$ for any $b:B$, where $\eta:B\to \sharp B$ is the unit of $\sharp$.
Now fix $y:\sharp B$ and $x:A^\sharp(y)$. For any $b:B$ and $p:\eta(b)=y$, we can define the type ${\big\Vert \sum_{(a:A(b))} p_\ast (\eta(a)) = x\big\Vert}_n$. This is an $n$-type, and since $n\text{-}Type$ is an $(n+1)$-type, as a function of $(b,p) : \sum_{b:B} \eta(b)=y$, this construction factors through $\big\Vert \sum_{b:B} \eta(b)=y\big\Vert_{n+1}$. Thus, for $y:\sharp B$ and $x:A^\sharp(y)$ and $\xi : {\big\Vert \sum_{(b:B)} \eta(b)=y\big\Vert}_{n+1}$ we have a type $P(y,x,\xi)$, such that
$P\big(y,x,{|(b,p)|}_{n+1}\big) = {\left\Vert \sum_{(a:A(b))} p_\ast (\eta(a)) = x\right\Vert}_n.$Now by definition, $\sharp_{n+1} B \coloneqq \sum_{(y:\sharp B)} {\big\Vert \sum_{(b:B)} \eta(b)=y\big\Vert}_{n+1}$. Thus, we can define $A^{\sharp_n} : \sharp_{n+1} B \to Type$ by $A^{\sharp_n}(y,\xi) = \sum_{x:A^\sharp(y)} P(y,x,\xi)$. And since $\eta_{n+1}(b) = (\eta(b),{|(b,1)|}_{n+1})$, we have $A^{\sharp_n}(\eta_{n+1}(b)) = \sum_{x:\sharp(A(b))} {\big\Vert \sum_{(a:A(b))} \eta(a)) = x\big\Vert}_n$, which is $\sharp_{n}(A(b))$ by definition.
Of course, this uses univalence and lex-ness of $\sharp$, whereas your #11 seemingly needs only that $\sharp$ preserves products. However, I think without univalence and lex-ness, we can’t identify $\mathbf{B}(\sharp_{n} G)$ with $\sharp_{n+1} (\mathbf{B}G)$, so those assumptions may be unavoidable when working elementarily.
Thanks a million! I am looking at it now…
Yeah, so this seems quite excellent. Thanks again! It also helps me to see the kind of argument you use, I should try to get more into the habit of reasoning in this style myself.
That makes perfect sense that an elementary proof needs univalence where the argument via simplicial objects needs the $\infty$-Giraud axioms.
In my note I’ll stick for the moment with the non-elementary argument, but if there is a way to cite you for the above, I’ll gladly do.
Let me just mention again what I am using the above result for:
Given an object $A$ equipped with a co-filtration $F^\bullet A$, say its concretification is the iterated homotopy fiber product
$Conc(A) \coloneqq \sharp_1 F^0 A \underset{\sharp_1 F^{1}A}{\times} \sharp_2 F^{1}A \underset{\sharp_2 F^{2}A }{\times} \cdots$Now given an $X$, I want to argue that $Aut(X)$ acts on $Conc([X,A])$ by using that, by the above, we have a natural system of fiber sequences
$\sharp_n [X,F^p A] \longrightarrow (\sharp_n [X,F^p A])/\sharp_n Aut(X) \longrightarrow \mathbf{B}\sharp_n Aut(X)$as $n$ and $p$ range, and then forming the above iterated fiber product in all three places of these sequences. On the left this gives $Conc([X,A])$ by definition. On the right (using the trivial co-filtration on $\mathbf{B}Aut(X)$) it gives $\sharp_\infty \mathbf{B}Aut(X) \simeq \mathbf{B} Aut(X)$. Since the limits commute over each other, we end up with a fiber sequence of the form
$Conc([X,A]) \longrightarrow Conc([X,A])/Aut(X) \longrightarrow \mathbf{B}Aut(X)$Well, I suppose you could cite this page. I don’t fully understand yet what’s going on theoretically with these concretifications — they seem to be part of a bigger story waiting to be told about separated objects relative to pairs of modalities or something — so I don’t think I’m ready to write a blog post or anything.
How about moving it to the $n$Lab. I made a start here. If you don’t like it, we’ll revert it.
That’s fine!
My current suspicion is that the underlying general facts here are something like
Given two modalities $\bigcirc$ and $\lozenge$ satisfying some relationship (e.g. $\lozenge$ preserves $\bigcirc$-modal maps, maybe more) there is a new modality $\lozenge_{\bigcirc}$ defined as the $\bigcirc$-image of the $\lozenge$-unit.
Given two modalities $\bigcirc$ and $\odot$ with the property that the $\odot$-modal types are the ones whose path-spaces are all $\bigcirc$-modal (and perhaps something else), it is sensible to define $\mathbf{B} (\bigcirc G)$ to be $\odot(\mathbf{B}G)$.
If $\bigcirc$ and $\lozenge$ satisfy property (1), and so do $\odot$ and $\lozenge$, while $\bigcirc$ and $\odot$ satisfy property (2), then $\lozenge_\bigcirc$ and $\lozenge_\odot$ also satisfy property (2).
$n$-truncation and $(n+1)$-truncation always satisfy property (2).
If $\lozenge$ is lex, then it satisfies property (1) when $\bigcirc$ is $n$-truncation, for any $n$.
Ah, okay, interesting. In this generality it would now be good to think about separated types. We want the analog of a modality unit being a mono in a situation where there is not a single concept of mono. So the $\bigcirc$s come in a tower of $\bigcirc_n$-s and on $\bigcirc_0$-modal types it makes direct sense to ask whether they are $\lozenge_1$-modal, where $\lozenge_1$ is the $\bigcirc_1$ of the $\lozenge$-unit. More generally on $\bigcirc_n$-modal types $X$, however,it seems to me that one needs to equip $X$ itself with a co-filtration and then define being $\lozenge$-modal by “intertwining” the degrees of this co-filtration with the $\bigcirc$-filtration on $\lozenge$.
What do you mean by “direct sense”? And what do you mean by “$\lozenge$-modal” in the last sentence — I gather it must be something other than the usual meaning?
Sorry, I was just rephrasing the concretification construction from #18 in the general abstract language that you started in #22.
Let’s switch back to the concrete example, to be less confusing:
In a local 1-topos, of course, the $\sharp$-“separated” or “concrete” objects are just the $\sharp_1$-modal once. That’s what I meant by “makes direct sense”.
Now the big question used to be what replaces this in a local $\infty$-topos. Back in hgp I had found the answer to this question by looking at what it has to be “in practice”, i.e. by finding a modal type theoretic formula that gives the “correct” (in practice) concretification of a higher differential moduli stack.
Namely one has to pick a co-filtration $F^\bullet X$ on the moduli stack (and in the canonical examples it’s an old friend, it’s the Hodge filtration!) and then the concretification is given by the iterated homotopy fiber product
$Conc(X^\bullet) := \sharp_1 F^0 X \underset{\sharp_1 F^1 X}{\times} \sharp_2 F^1 X \underset{\sharp_2 F^2 X}{\times} \sharp_3 F^2 X \times \cdots \,.$Take the co-filtration to be $X \to \ast \to \ast \to \cdots$, then this collapses to $\sharp_1 X$. On the other extreme, take the co-filtration to be constant on $X$, then this reproduces $X$. So this is a concretification relative to a choice of co-filtering. At first this looked unexpected. But the more I look at it the more I feel that probably some instance of this kind of construction is well known somewhere in the literature.
Ok, so by “$\lozenge$-modal” you meant something like “$\lozenge$-concrete”?
Also, is the indexing off or shifted? I would have thought that the separated/concrete objects in a 1-topos would be the $\sharp_{-1}$-modal ones.
Ah right, I should have said $\lozenge$-concrete (or separated).
With the counting I thought I’d rather say “1-image” than “$(-1)$-image” and start counting at 0 instead of at $(-2)$. But, yeah, it’s the usual annoying $\pm 2$ offset.
The real problem with offsetting, I think, is that then it doesn’t generalize to other modalities. We can define $\lozenge_\bigcirc$ for any $\lozenge$ and $\bigcirc$, and then specializing to $\bigcirc = n$-truncation means we really ought to write $\lozenge_n$ in that case, not $\lozenge_{n+2}$.
We ought to write $\lozenge_{\tau_n}$ and I am inclined to opt for declaring that $\lozenge_{n+2}$ is alternative notation for this.
While for “truncation” starting to count at $-2$ is nice because it matches the traditional counting of homotopy groups, for “image” starting to count at $-2$ makes the traditional image be a $(-1)$-image, while any traditional thing we’d rather have to be a 1-thing or a 0-thing, but not a $(-1)$-thing.
Of course it’s not important. If you prefer to speak of the (-1)-image (as I suppose the book does) I won’t quarrel with it.
There are lots of other places where we write $n$ in place of $\tau_n$ (e.g. $n$-connected maps), so I think it would be confusing to instead write $n+2$ in place of $\tau_n$ here.
1 to 30 of 30