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
   • CommentTimeNov 29th 2012
   • (edited Nov 29th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex(...)

   (…)

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 29th 2012
   • (edited Nov 29th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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?

   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?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, it appears to be an equivalence when $n=1$ and $n=\infty$...

   Well, it appears to be an equivalence when $n=1$ and $n=\infty$…

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJan 19th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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?

   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?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 19th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexLet'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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 19th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexRight, 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...

   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…

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 19th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJan 19th 2015
   • (edited Jan 19th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, 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](http://ncatlab.org/nlab/show/concretification#DifferentialConcretificationForAbelianNConnections), which is an iterated fiber product of $n$-images of the sharp unit. Need to dash off now...

   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…

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 19th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIf 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. (-:

   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. (-:

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, 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?

    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?

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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?

    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?

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexSo 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 } $$ ?

    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 }$$

    ?

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhy is the middle column a fiber sequence in the case of looping?

    Why is the middle column a fiber sequence in the case of looping?

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have sent you an email on this.

    I have sent you an email on this.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHmm, 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?

    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?

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHere'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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks a million! I am looking at it now...

    Thanks a million! I am looking at it now…

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2015
    • (edited Jan 20th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYeah, 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 [[schreiber:Obstruction theory for parameterized higher WZW terms|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) $$

    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)$$
19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, 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.

    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.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexHow about moving it to the $n$Lab. I made a start [here](http://ncatlab.org/nlab/show/infinity-action#CoDiscretizationOfActions). If you don't like it, we'll revert it.

    How about moving it to the $n$Lab. I made a start here. If you don’t like it, we’ll revert it.

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThat's fine!

    That’s fine!

22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexMy current suspicion is that the underlying general facts here are something like 1. 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. 2. 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)$. 3. 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). 4. $n$-truncation and $(n+1)$-truncation always satisfy property (2). 5. If $\lozenge$ is lex, then it satisfies property (1) when $\bigcirc$ is $n$-truncation, for any $n$.

    My current suspicion is that the underlying general facts here are something like

    1. 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.

    2. 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)$.

    3. 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).

    4. $n$-truncation and $(n+1)$-truncation always satisfy property (2).

    5. If $\lozenge$ is lex, then it satisfies property (1) when $\bigcirc$ is $n$-truncation, for any $n$.

23. • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, 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$.

    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$.

24. • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat 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?

    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?

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexSorry, 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 [[schreiber:Higher geometric prequantum theory|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.

    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.

26. • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOk, 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.

    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.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh 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.

    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.

28. • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe 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}$.

    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}$.

29. • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJan 23rd 2015
    • (edited Jan 23rd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexWe 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.

    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.

30. • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThere 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.

    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.