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
    • CommentTimeApr 28th 2015
    • (edited Apr 28th 2015)

    Given any object VV in an elementary \infty-topos, then its automorphism group Aut(V)\mathbf{Aut}(V) may be characterized as the pointed connected object which is the 1-image of the name of VV in the type universe.

    Now if VV itself has group structure, hence if there is pointed connected *BV\ast \to \mathbf{B}V, what is the elementary way to speak of its group Aut Grp(V)\mathbf{Aut}_{Grp}(V) of group automorphisms, hence of automorphisms of BV\mathbf{B}V that preserve the basepoint?

    And I’d need a canonical forgetful map

    Aut Grp(V)Aut(V). \mathbf{Aut}_{Grp}(V) \longrightarrow \mathbf{Aut}(V) \,.
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2015

    Hm, I know how to elementarily get Aut Grp(V)Aut(BV)\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(\mathbf{B}V), as this is the stabilizer group (by the discussion there) of (*BV)[*,BV](\ast \to \mathbf{B}V) \in [\ast,\mathbf{B}V] under the right Aut(BV)\mathbf{Aut}(\mathbf{B}V)-action. But I am not sure how to get the map to Aut(V)\mathbf{Aut}(V).

    I see that I have another problem of similar nature. Given a homotopy pullback

    X 2 B 2 X 1 ϕ B 1 \array{ X_2 &\longrightarrow& B_2 \\ \downarrow && \downarrow \\ X_1 &\stackrel{\phi}{\longrightarrow}& B_1 }

    then the automorphisms of X 1X_1 over B 1B_1 should canonically act on X 2X_2. The elementary construction o the former is again as the stabilizer of ϕ[X 1,B 1]\phi\in [X_1,B_1] under Aut(X 1)\mathbf{Aut}(X_1). But how to construct the action of that on X 2X_2 by elementary means?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeApr 28th 2015

    A simpler way to get Aut Grp(V)Aut_{Grp}(V) is as e:BVBV(e(pt)=pt)\sum_{e:B V \simeq B V} (e(pt) = pt). To get the map to Aut(V)Aut(V) you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

    In the second question, if you represent X 1X_1 as a type family X 1:B 1TypeX_1 : B_1 \to Type, then its automorphisms over B 1B_1 are b:B 1Aut(X 1(b))\prod_{b:B_1} Aut(X_1(b)). Then X 2X_2 is just the composite B 2gB 1TypeB_2 \xrightarrow{g} B_1 \to Type and an f: b:B 1Aut(X 1(b))f:\prod_{b:B_1} Aut(X_1(b)) sends x:X 2(a)x:X_2(a) (i.e. x:X 1(g(a))x:X_1(g(a))) to f(g(a),x)f(g(a),x).

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2015
    • (edited Apr 28th 2015)

    Thanks, Mike, but wait:

    A simpler way to get Aut Grp(V)Aut_{Grp}(V) is as e:BVBV(e(pt)=pt)\sum_{e:B V \simeq B V} (e(pt) = pt).

    That translates semantically to the homotopy fiber of Aut(BV)()pt[*,BV]\mathbf{Aut}(\mathbf{B}V) \stackrel{(-) \circ pt}{\longrightarrow} [\ast, \mathbf{B}V], which is what I recognize as the stabilizer group of ptpt under the canonical Aut(BV)\mathbf{Aut}(\mathbf{B}V)-action on [*,BV][\ast,\mathbf{B}V]. So this I am happy with, but I have trouble formalizing this sentence:

    To get the map to Aut(V)Aut(V) you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

    Of course I know that this is so, externally, but which universal construction gets me the map out of the above homotopy fiber?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeApr 28th 2015

    Oh, it’s just so much easier to think internally… (-:

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2015
    • (edited Apr 28th 2015)

    Oh, it’s just so much easier to think internally… (-:

    I certainly see that, it is indeed much easier, indeed it’s close to being effortless, in that to a large extent one just makes the naive statements. It’s beautiful.

    But either I am missing something, or I really do need the translation of this effortless language to diagrams, because as a second step after having the internal formulation of something, I need to extract some actual maps of stacks out of it.

    Concretely, right now I am chewing on the following: I have an abstract internal construction of a class of higher groups which externalizes to the super-groups Lie integrating the M-theory super Lie algebra with its degree-2 extension (we have an article on that essentially done, details should be available in a short while).

    But the full M-theory super Lie algebra involves also a degree-5 extension piece. I think I know which internal construction gives that, too. But to check, I need to translate that to an actual universal construction of super stacks, and work out if it comes out as it should.

    Maybe I am being dense, but it seems to me for that I really need some universal pullback diagram of sorts that constructs for me that map of group stacks Aut Grp(V)Aut(V)\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(V).

    Now I know how to translate any actual formula that you write in homotopy type theory into such universal constructions. But I don’t know what to do concretely in this respect when you say infromal things like

    you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeApr 28th 2015

    Yes, I know that sometimes we really do need to extract a diagrammatic statement from the internal reasoning. (That’s why I put a smiley on my comment.) I don’t have time to do the extraction right now, but if you’re willing to do it, here’s a formula: given (e,t): e:BVBV(e(pt)=pt)(e,t) : \sum_{e:B V \simeq B V} (e(pt) = pt), we define Ωe:ΩBVΩBV\Omega e : \Omega B V \to \Omega B V by Ωe(p)=t 1ap e(p)t\Omega e (p) = t^{-1} \cdot ap_e(p) \cdot t. Here p:pt= BVptp : pt =_{B V} pt, so ap e(p):e(pt)=e(pt)ap_e(p) : e(pt) = e(pt), and conjugating it by tt brings it back to pt=ptpt = pt again, i.e. ΩBV\Omega B V.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2015
    • (edited Apr 28th 2015)

    Thanks. Here is what I have now come up with:

    Consider the squares

    Aut Grp(V) Aut Grp(V)×BV * * BV * \array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longleftarrow& \ast \\ \downarrow && \downarrow && \downarrow \\ \ast &\longrightarrow& \mathbf{B}V &\longleftarrow& \ast }

    where the left one is obtained from factoring the defining pullback square of Aut Grp(V)Aut(BV)×BV*\mathbf{Aut}_{Grp}(V) \simeq \mathbf{Aut}(\mathbf{B}V) \underset{\mathbf{B}V}{\times} \ast as

    Aut Grp(V) Aut(BV) Aut Grp(V)×BV Aut(BV)×BV ev * BV \array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}(\mathbf{B}V) \\ \downarrow && \downarrow \\ \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longrightarrow& \mathbf{Aut}(\mathbf{B}V) \times \mathbf{B}V \\ \downarrow && \downarrow^{\mathrlap{ev}} \\ \ast &\longrightarrow& \mathbf{B}V }

    Then forming homotopy limits over the horizontal cospans in the first two squares yields a map

    Aut Grp(V)×VV \mathbf{Aut}_{Grp}(V) \times V \longrightarrow V

    The adjunct of that might factor through the map Aut Grp(V)Aut(V)\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(V) that I am after.

    Hm, this needs more checking. But I need to quit now.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • (edited Apr 29th 2015)

    Ah, or rather I should take also the right square to be (the horizontal reverse of) that left square, and that then gives the conjugation action that you indicated.

    (Aut Grp(V)×V V)=lim(Aut Grp(V) Aut Grp(V)×BV Aut Grp(V) * BV *) \left( \array{ \mathbf{Aut}_{Grp}(V) \times V \\ \downarrow \\ V } \right) \;\;= \;\; lim \left( \array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longleftarrow& \mathbf{Aut}_{Grp}(V) \\ \downarrow && \downarrow && \downarrow \\ \ast &\longrightarrow& \mathbf{B}V &\longleftarrow& \ast } \right)
    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015

    Okay, good, using this I have a formalization of the concept of BPS charges for branes without tensor multiplets (now section 5.3.13 here). Now to generalize further and have BPS charges for branes with tensor multiplets I need a similar diagrammatic answer for the second question in #2.

    But first some lunch now.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeApr 29th 2015

    Great! Is the internal description I gave in #3 sufficient for you to extrarct a diagrammatic answer?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • (edited Apr 29th 2015)

    Here I’d like to rephrase the method in #3 in terms of homotopy fibers again, using

    Aut B 1(X 1) B 1Aut(ϕ) fib(Aut(X 1)ϕ()[X 1,B 1]) \begin{aligned} \mathbf{Aut}_{B_1}(X_1) &\coloneqq \underset{B_1}{\prod} \mathbf{Aut}(\phi) \\ &\simeq fib(\mathbf{Aut}(X_1)\stackrel{\phi\circ(-)}{\longrightarrow} [X_1,B_1]) \end{aligned}

    because that makes it easier to adopt this to the case where this group needs to be differentially concretified before acting, which happens to be the case that I really need.

    Then the following should be a solution: we observe the pasting composite

    Aut B 1(X 1)×X 1 Aut(X 1)×X 1 ev X 1 p 2 (ϕ(),id) ϕ X 1 (ϕ,id) [X 1,B 1]×X 1 ev B 1 ϕ id B 1 = B 1 = B 1 \array{ \mathbf{Aut}_{B_1}(X_1) \times X_1 &\longrightarrow& \mathbf{Aut}(X_1) \times X_1 &\stackrel{ev}{\longrightarrow}& X_1 \\ \downarrow^{\mathrlap{p_2}} && \downarrow^{\mathrlap{(\phi\circ(-),id)}} && \downarrow^{\phi} \\ X_1 &\stackrel{(\vdash\phi,id)}{\longrightarrow}& [X_1,B_1] \times X_1 &\stackrel{ev}{\longrightarrow}& B_1 \\ \downarrow^{\mathrlap{\phi}} && && \downarrow^{\mathrlap{id}} \\ B_1 &=& B_1 &=& B_1 }

    where the top left square is the image under ()×X 1(-)\times X_1 of the pullback square that exhibits the homotopy fiber just mentioned, and where the right square is the Hom-adjunct of a trivially commuting square expressing postcomposition with ϕ\phi.

    Now we base change the outer diagram along B 2B 1B_2\to B_1 to get an action morphism

    Aut B 1(X 1)×X 2X 2 \mathbf{Aut}_{B_1}(X_1) \times X_2 \longrightarrow X_2

    together with a square that exhibits this action as being over B 2B_2.

  1. Re #1: I’m trying to understand what

    the name of V in the type universe U

    means.

    Is it the arrow f:1Uf:1\to U corresponding to V1V\to1 as described in universe in a topos? A quick search didn’t lead to any other reference explaining the terminology.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015

    Yes!

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • (edited Apr 29th 2015)

    The univalent type universe TypeType aka object classifier in an infinity-topos has the property that every map XBX \to B with sufficiently small homotopy fiber sits in a homotopy pullback of the form

    X Type^ B Type \array{ X &\longrightarrow& \widehat {Type} \\ \downarrow && \downarrow \\ B &\longrightarrow& Type }

    Here the bottom horizontal map, which “classifies” or “modulates” XX is “the name of XX”.

  2. Thanks for the explanation. Is the terminology standard? I couldn’t find it on the other page you linked to.

    Is there a similar terminology for the upper horizontal arrow in your last diagram and the object Type^\widehat {Type}?

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015
    • (edited Apr 30th 2015)

    I didn’t make up this terminology, it is used in circles of category theorists, but the circle that uses it may not be huge. You see it for instance in the first line here. I agree that it would be good to have this better documented on the nnLab. If anyone has time and energy, please do.

    Todd Trimble is likely to know references. If he doesn’t see this here, maybe email him.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 30th 2015

    I’m not sure I do know good references. You can find internal universes in pretoposes used in Algebraic Set Theory for instance (see the monograph by Joyal and Moerdijk).

  3. Thanks again. Concerning the diagram in #15, with an arbitrary BB which is not necessarily the terminal object, wouldn’t it be more “correct” to say: “the images of BTypeB\to Type are the names of the fibers of XBX\to B”.

    This could be nitpicking or just a lack of understanding from my part :)

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015

    Michael, maybe you are taking a casual choice of terminology more serious than it ought to. It being terminology, there is no way it could be “correct” or “incorrect”.

    I would say that BTypeB \to Type is the name of all of XX and its restrictions along any *BType\ast \to B \to Type are the names of the fibers. But if you don’t like that choice of wording, that’s fine, too.

    Over at propositional extensionality this issue is dealt with by quotation marks. For PP a proposition, then P'P' is its name (this PP is XX from before, just a different symbol, same idea). I think it makes very good sense.

    If you feel idealistic, you might call P'P' the inner reflection of the outer PP. :-)

  4. Agreed that there is no objective way in which terminology is correct or incorrect. I was not sure I understood the idea behind the terminology, but I think it’s clear now.

    Your last sentence, on the other hand, gives me new food for thought :) But I don’t want to hijack this thread any longer.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015
    • (edited Apr 30th 2015)

    Michael,

    please, it’s good to discuss this, and given that apparently the nnLab entries didn’t convey this, we should strive to edit them.

    I am a bit too busy with something else to edit right now. But to the extent that you feel you gained information here that wasn’t on the nnLab pages then you are invited, I’d even say urged and would like to say: compelled, to add it in. Please do, to the extent that you feel certain.

    To the extent that you don’t feel certain yet, just open another thread here dedicated to the issue!