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
    • CommentTimeNov 29th 2012
    • (edited Nov 29th 2012)

    (…)

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 29th 2012
    • (edited Nov 29th 2012)

    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

    A f B h α k C g D \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 BB and DD, we get a induced objects

    fib(im n(h)im n(k)) fib(im_n(h) \to im_n(k))

    and

    im n(fib(f)fib(g)) im_n(fib(f) \to fib(g))

    with a map from the latter to the former. How far is that from being an equivalence?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2012

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

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015

    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?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015

    Let’s see, probably some messing around with sigma-types will reduce it to the case when C=D=1C=D=1. In that case the naive question becomes “does nn-truncation preserve homotopy fibers?” And the answer to that is certainly no, e.g. if A=1A=1 as well then you’re comparing the nn-truncation of the loop space with the loop space of the nn-truncation, which are of course not the same — the latter is the further (n1)(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.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015

    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 hh and kk 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…

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015

    I think I see how to prove in general that the comparison map is (n1)(n-1)-connected. Since it’s automatically nn-truncated (being a map between nn-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.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)

    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(Σ)Aut(\Sigma)-action on [Σ,B n𝔾 conn][\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 nn-images of the sharp unit.

    Need to dash off now…

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015

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

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)

    Okay, now I am back. So it might just be enough, allow me think out loudly:

    I’ll write n\sharp_n for the nn-truncation of the unit of the sharp modality.

    Given an action of GG on VV exhibited by a fiber sequence

    VV/GBGV \to V/G \to \mathbf{B}G

    I’d like to have an action of nG\sharp_n G on nV\sharp_n V. So I hit the fiber sequence with n+1\sharp_{n+1} to get two consecutive maps

    n+1V n+1(V/G)B nG\sharp_{n+1}V\to \sharp_{n+1}(V/G) \to \mathbf{B} \sharp_n G

    and from what you say this almost exhibits n+1V\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 nV\sharp_n V instead, anyway, not on n+1V\sharp_{n+1}V. So maybe one may just further truncate on the left to get this?

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)

    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/GV/G is the homotopy colimit of the simplicial object (V/G) =G × ×V(V/G)_\bullet = G^{\times_\bullet} \times V.

    Now I am thinking: n\sharp_n preserves products. Because nn-image factorization satisfies im n(X 1×Y 1(f,g)X 2×Y 2)(im n(f)×im n(g)X 2×Y 2)\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 nn-truncation preserves products and because we may write (f,g)(f,g) as a product of (f,id)(f,id) with (id,g)(id,g) in the slice over X 2×Y 2X_2 \times Y_2.

    So that makes me think that from the simplicial object (V/G) (V/G)_\bullet I get a simplicial object ( n(V)/ n(G)) =( nG) × × nV(\sharp_n(V)/\sharp_n(G))_\bullet = (\sharp_n G)^{\times_\bullet}\times \sharp_n V. And this finally exhibits an induced action of nG\sharp_n G on nV\sharp_n V.

    Does that seem right?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)

    So in the special case of looping of a morphism f:XYf \colon X \to Y of pointed objects, we have a diagram of the form

    Ωf: ΩX im n(Ωf) ΩY id *: * im n+1(id *)* * f: X im n+1(f) Y \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

    fib(α) im n(fib(ϕ)) fib(β) g: X 1 im n+1(g) Y 1 α ϕ β f: X 2 im n+1(f) Y 2 \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 }

    ?

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015

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

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2015
    • (edited Jan 19th 2015)

    I have sent you an email on this.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2015

    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=*X_2 = Y_2 = \ast, then fib(α)=X 1fib(\alpha)=X_1 and fib(β)=Y 1fib(\beta) = Y_1 and fib(ϕ)=gfib(\phi) = g, but the nn-image and the (n+1)(n+1)-image of gg are not the same. Of course in that case one has instead a fiber sequence with im n+1(fib(ϕ))im_{n+1}(fib(\phi)) at the top.

    But #11 does sound plausible. Is n\sharp_n by any chance a modality in its own right?

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2015

    Here’s a HoTTer way to make nG\sharp_n G act on nV\sharp_n V. Let A:BTypeA:B\to Type be any type family; I claim there is an induced family A n: n+1BTypeA^{\sharp_n} : \sharp_{n+1} B \to Type such that A n(η n+1(b))= n(A(b))A^{\sharp_n}(\eta_{n+1}(b)) = \sharp_n (A(b)) for any b:Bb:B, where η n+1:B n+1B\eta_{n+1} : B \to \sharp_{n+1} B is the inclusion. Applying this when bb is the basepoint of BG\mathbf{B}G should give the desired action on the desired type.

    First of all, we have the composite BATypeType B \xrightarrow{A} Type \xrightarrow{\sharp} Type_{\sharp}, where Type = X:Typeis(X)Type_{\sharp} = \sum_{X:Type} is\sharp(X). Since Type Type_{\sharp} is itself \sharp (since \sharp is lex), this factors through B\sharp B, giving a type family A :BType A^\sharp : \sharp B \to Type_{\sharp} such that A (η(b))=(A(b))A^{\sharp}(\eta(b)) = \sharp (A(b)) for any b:Bb:B, where η:BB\eta:B\to \sharp B is the unit of \sharp.

    Now fix y:By:\sharp B and x:A (y)x:A^\sharp(y). For any b:Bb:B and p:η(b)=yp:\eta(b)=y, we can define the type (a:A(b))p *(η(a))=x n{\big\Vert \sum_{(a:A(b))} p_\ast (\eta(a)) = x\big\Vert}_n. This is an nn-type, and since n-Typen\text{-}Type is an (n+1)(n+1)-type, as a function of (b,p): b:Bη(b)=y(b,p) : \sum_{b:B} \eta(b)=y, this construction factors through b:Bη(b)=y n+1\big\Vert \sum_{b:B} \eta(b)=y\big\Vert_{n+1}. Thus, for y:By:\sharp B and x:A (y)x:A^\sharp(y) and ξ: (b:B)η(b)=y n+1\xi : {\big\Vert \sum_{(b:B)} \eta(b)=y\big\Vert}_{n+1} we have a type P(y,x,ξ)P(y,x,\xi), such that

    P(y,x,|(b,p)| n+1)= (a:A(b))p *(η(a))=x n.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, n+1B (y:B) (b:B)η(b)=y n+1\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 n: n+1BTypeA^{\sharp_n} : \sharp_{n+1} B \to Type by A n(y,ξ)= x:A (y)P(y,x,ξ)A^{\sharp_n}(y,\xi) = \sum_{x:A^\sharp(y)} P(y,x,\xi). And since η n+1(b)=(η(b),|(b,1)| n+1)\eta_{n+1}(b) = (\eta(b),{|(b,1)|}_{n+1}), we have A n(η n+1(b))= x:(A(b)) (a:A(b))η(a))=x nA^{\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 n(A(b))\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 B( nG)\mathbf{B}(\sharp_{n} G) with n+1(BG)\sharp_{n+1} (\mathbf{B}G), so those assumptions may be unavoidable when working elementarily.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2015

    Thanks a million! I am looking at it now…

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2015
    • (edited Jan 20th 2015)

    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 AA equipped with a co-filtration F AF^\bullet A, say its concretification is the iterated homotopy fiber product

    Conc(A) 1F 0A× 1F 1A 2F 1A× 2F 2A 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 XX, I want to argue that Aut(X)Aut(X) acts on Conc([X,A])Conc([X,A]) by using that, by the above, we have a natural system of fiber sequences

    n[X,F pA]( n[X,F pA])/ nAut(X)B nAut(X) \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 nn and pp range, and then forming the above iterated fiber product in all three places of these sequences. On the left this gives Conc([X,A])Conc([X,A]) by definition. On the right (using the trivial co-filtration on BAut(X)\mathbf{B}Aut(X)) it gives BAut(X)BAut(X)\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])Conc([X,A])/Aut(X)BAut(X) Conc([X,A]) \longrightarrow Conc([X,A])/Aut(X) \longrightarrow \mathbf{B}Aut(X)
    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2015

    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.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2015

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

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2015

    That’s fine!

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    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 B(G)\mathbf{B} (\bigcirc G) to be (BG)\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. nn-truncation and (n+1)(n+1)-truncation always satisfy property (2).

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

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    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 \bigcircs come in a tower of n\bigcirc_n-s and on 0\bigcirc_0-modal types it makes direct sense to ask whether they are 1\lozenge_1-modal, where 1\lozenge_1 is the 1\bigcirc_1 of the \lozenge-unit. More generally on n\bigcirc_n-modal types XX, however,it seems to me that one needs to equip XX 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.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    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?

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    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 1\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 XF^\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 ):= 1F 0X× 1F 1X 2F 1X× 2F 2X 3F 2X×. 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**X \to \ast \to \ast \to \cdots, then this collapses to 1X\sharp_1 X. On the other extreme, take the co-filtration to be constant on XX, then this reproduces XX. 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.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2015

    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 1\sharp_{-1}-modal ones.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2015
    • (edited Jan 22nd 2015)

    Ah right, I should have said \lozenge-concrete (or separated).

    With the counting I thought I’d rather say “1-image” than “(1)(-1)-image” and start counting at 0 instead of at (2)(-2). But, yeah, it’s the usual annoying ±2\pm 2 offset.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    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 =n\bigcirc = n-truncation means we really ought to write n\lozenge_n in that case, not n+2\lozenge_{n+2}.

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJan 23rd 2015
    • (edited Jan 23rd 2015)

    We ought to write τ n\lozenge_{\tau_n} and I am inclined to opt for declaring that n+2\lozenge_{n+2} is alternative notation for this.

    While for “truncation” starting to count at 2-2 is nice because it matches the traditional counting of homotopy groups, for “image” starting to count at 2-2 makes the traditional image be a (1)(-1)-image, while any traditional thing we’d rather have to be a 1-thing or a 0-thing, but not a (1)(-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.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2015

    There are lots of other places where we write nn in place of τ n\tau_n (e.g. nn-connected maps), so I think it would be confusing to instead write n+2n+2 in place of τ n\tau_n here.