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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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
    • CommentTimeJun 30th 2012

    started an entry infinity-action

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 16th 2012
    • (edited Sep 16th 2012)

    I have been expanding at infinity-action in an attempt to make the discussion more comprehensive and more coherent. But not done yet.

    For instance I made explicit that for c:BGV(c):Type\mathbf{c} : \mathbf{B}G \vdash V(\mathbf{c}) : Type an \infty-action we have

    • the dependent product

      c:BGV(c):Type \vdash \prod_{\mathbf{c} : \mathbf{B}G}V(\mathbf{c}) : Type

      is the type of invariants of the action;

    • the dependent sum

      c:BGV(c):Type \vdash \sum_{\mathbf{c} : \mathbf{B}G}V(\mathbf{c}) : Type

      is the quotient of the action

    And hence for V 1V_1 and V 2V_2 two actions we have that

    • c:BGV 1(c)V 2(c):Type\vdash \prod_{\mathbf{c} : \mathbf{B}G} V_1(\mathbf{c}) \to V_2(\mathbf{c}) : Type

      is the type of GG-homomorphisms (of GG-equivariant maps);

    • c:BGV 1(c)V 2(c):Type\vdash \sum_{\mathbf{c} : \mathbf{B}G} V_1(\mathbf{c}) \to V_2(\mathbf{c}) : Type

      is the quotient of all maps by the GG-cojugation action.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 24th 2012

    Added at infinity-action brief remarks in new subsections

    This is more to remind myself to come back to it later. No time right now.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMar 5th 2014

    added to infinity-action under a new section References – For discrete geometry pointers to articles that discuss GAct Grpd /BGG Act_\infty \simeq \infty Grpd_{/ B G}.

    (copied the same also to the end of the citations at principal infinity-bundle).

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2014
    • (edited Mar 11th 2014)

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeApr 14th 2014
    • (edited Apr 14th 2014)

    added now also a new section References – For actions of topological groups with the following text (which might also go into a Properties-section, admittedly):

    [ text extracted from entry ]

    That GG-actions for GG a topological group in the sense of G-spaces in equivariant homotopy theory (and hence with GG not regarded as the geometrically discrete ∞-group of its underying homotopy type ) are equivalently objects in the slice (∞,1)-topos over BG\mathbf{B}G is Elmendorf’s theorem together with the fact, highlighted in this context in


    GSpacePSh (Orb G)PSh (Orb /BG)PSh (Orb) /BG G Space \simeq PSh_\infty(Orb_G) \simeq PSh_\infty(Orb_{/\mathbf{B}G}) \simeq PSh_\infty(Orb)_{/\mathbf{B}G}

    is therefore the slice of the \infty-topos over the slice of the global orbit category over BG\mathbf{B}G.

    !include equivariant homotopy theory – table

    See at equivariant homotopy theory for more references along these lines.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

    added a little observation – here – on how the automorphism action on an object in a slice is given by descending the corresponding map to the homotopy quotient of the induced action on the dependent sum.

    (This innocent statement gives symplectic reduction for prequantum n-bundles)

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 4th 2015

    There is a nice formalization of linearization of \infty-actions in axiomatics of differential cohesion. I have added it to the entry here.

    (The text deserves further polishing, but I am in a haste now as my battery is dying.)

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 4th 2015

    I have now written this (linearization of \infty-actions) out in more detail in section 3.10.5 of dcct (pdf).

    In section 3.10.11 I use this to axiomatize Cartan geometry in differential cohesion, via the key example (3.10.45) of the canonical linearized HH action on 𝔤/𝔥\mathfrak{g}/\mathfrak{h} .

    (I have been fiddling with the axiomatization of Cartan geometry in homotopy-type theory a bit, as you may recall. My first versions were not so good, but I think now I am converging.)

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2015
    • (edited Apr 16th 2015)

    Added an expositional section Examples – Discrete group actions on sets which spells out in detail how the general abstract slicing perspective recovers ordinary permutation representations.

    I should maybe copy this also to, or at least link to also from, action groupoid and permutation representation.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2020

    added publication data to:

    • Amit Sharma, On the homotopy theory of GG-spaces, International Journal of Mathematics and Statistics Invention, Volume7 Issue 2 (arXiv:1512.03698, published pdf)

    diff, v41, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2020

    added publication data to:

    diff, v41, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    cross-linked the example of the adjoint action (here) with free loop space of a classifying space

    diff, v42, current

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 4th 2021

    I was pointing David Spivak to the adjoint action over here. I think that’s right about why conjugation appears as an example of his ’jump’ monad.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    I have followed the link now, but would need to have a closer look.

    To see the conjugation action (or any action) naturally from homotopy type theory one needs at least homotopy 1-types, in order to have 0-truncated groups (at least) realized as GΩBGG \simeq \Omega \mathbf{B}G. Does Spivak mean to consider this?

    A type-theory language account on these matters is, of course, in Buchholtz, van Doorn, Rijke’s arXiv:1802.04315. They briefly mention the conjugation action on p. 11, though they just seem to recall the folklore there.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 4th 2021

    Well, he seems to be looking to understand the algebraic structure of dependent type theory syntax:

    The fact that conjugation is an example of this structure is interesting, but it also means that the structure does not completely characterize dependent type syntax:

    My suspicion is that conjugation is appearing as a case of internal-hom as a kind of exponential.

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    If a type in H/BG\mathbf{H}/\mathbf{B} G is a GG \infty-action, what’s a dependent type there, so *:BG,v:V(*)W(*,v):Type\ast : \mathbf{B} G, v: V(\ast) \vdash W(\ast, v): Type? Does that amount to a kind of equivariant bundle?

    So if WW is a principal bundle over VV, then if all is in the context of BG\mathbf{B} G that’s why the Γ\Gamma at equivariant principal bundle needs to be considered with a GG-action?

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    Yes, absolutely. I had tried to have a discussion on this in a thread elsewhere.

    So for GG any \infty-group, a “GG-equivariant \infty-group” Γ\Gamma should be a group-object in the slice H /BG\mathbf{H}_{/\mathbf{B}G}. I still don’t quite understand these in full generality, but I understand the following sub-class:


    1) If Γ\Gamma is a group in H\mathbf{H} which is equipped with a GG-action by group automorphisms, then (a) ΓGGroups(H /BG)\Gamma \sslash G \in Groups(\mathbf{H}_{/\mathbf{B}G}) and (b) B(ΓG)(BΓ)G\mathbf{B}(\Gamma \sslash G) \simeq (\mathbf{B}\Gamma) \sslash G.

    2) The GG-equivariant \infty-groups of this form are equivalent to split \infty-group extensions in H\mathbf{H} of the form ΓhofibΓGG\Gamma \overset{hofib}{\longrightarrow} \Gamma \rtimes G \to G, under the identification (BΓ)GB(ΓG)(\mathbf{B}\Gamma) \sslash G \simeq \mathbf{B}(\Gamma \rtimes G).

    I think I have proof of these two statements (for what it’s worth, but it does require an argument that is not completely trivial, unless I am missing something).

    Moreover, I can see that the general group object in H /BG\mathbf{H}_{/\mathbf{B}G} is a structure very close to (1) and (2), but I still fail to see a proof that (1) and (2) exhaust the group objects in H /BG\mathbf{H}_{/\mathbf{B}G}.

    In any case, once we have such a group object in the slice over BG\mathbf{B}G, then the \infty-groupoid of GG-equivariant Γ\Gamma-principal \infty-bundles on GG-stacks XH /BGX \in \mathbf{H}_{/\mathbf{B}G} is

    GEquvΓPrinBdls(H) X=H /BG(XG,B(ΓG)) G Equv \Gamma PrinBdls(\mathbf{H})_{X} \;=\; \mathbf{H}_{/\mathbf{B}G} \big( X \sslash G, \; \mathbf{B}(\Gamma \sslash G) \big)

    For the cases in the class (1), (2), this subsumes the traditional notion of equivariant principal bundles, under the embedding DTopologicalSpacesCDfflgHSmoothGroupoids DTopologicalSpaces \xhookrightarrow{CDfflg} \mathbf{H} \coloneqq SmoothGroupoids_\infty.

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 6th 2021
    • (edited Jul 11th 2021)

    Presumably whatever HoTT delivers is right, so then it’s a question of interpreting any HoTT-reasoning in whatever (,1)(\infty, 1)-topos. E.g., if we have the abstract general theory of Γ\Gamma-principal bundles, then we just see what this amounts to in H /BG\mathbf{H}_{/\mathbf{B} G}.

    So that’s the issue with (1) and (2), whether these are the correct externalization of principal bundle theory internal to a (,1)(\infty, 1)-topos of the kind H /BG\mathbf{H}_{/\mathbf{B} G}?

    Hmm, what makes for externalization to be a non-trivial problem?

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    So (1) and (2) is certainly correct, in that they do yield a sub-\infty-groupoid of Groups(H /BG)Groups(\mathbf{H}_{/\mathbf{B}G}) and they do subsume the traditional external equivariant groups and equivariant bundles.

    I just don’t know if they exhaust Groups(H /BG)Groups(\mathbf{H}_{/\mathbf{B}G}). Hence I don’t know currently whether a “GG-equivariant \infty-group” could be slightly more general than being a semidirect product \infty-group ΓG\Gamma \rtimes G. (It seems unlikely, but I don’t have a proof.)

    I have re-installed the question on which I get stuck in the Sandbox.

    So where for ordinary topological groups we have an equivalence

    {semidirectproductswithG}Groups(GActions) \{semidirect\; products\;with\;G\} \xrightarrow{ \;\;\;\;\; \simeq \;\;\;\;\; } Groups(G Actions)

    for \infty-groups I currently only know that this map is a full embedding.

    This should be a minor technical issue, and not a big deal. If the map should really not be an equivalence, it would just mean that equivariant \infty-bundles could show a new structural phenomenon not seen in equivariant topological bundles. It feels like this is unlikely, though.

    • CommentRowNumber21.
    • CommentAuthorUlrik
    • CommentTimeJul 10th 2021

    A type-theory language account on these matters is, of course, in Buchholtz, van Doorn, Rijke’s arXiv:1802.04315. They briefly mention the conjugation action on p. 11, though they just seem to recall the folklore there.

    I’m not sure what you mean by “just”. We point out many results that are trivial to establish in the context of HoTT, but we weren’t aware of any HoTT folklore around them, except for what was in Mike’s café blog post. This didn’t discuss the adjoint action nor semi-direct products.

    We were short on space, so we couldn’t include many of the one-line proofs, unfortunately. (We chose to present the stabilization stuff in more detail, instead.)

    For instance, to see that G adG=LBGG^{ad} \sslash G = L B G, just note that

    G adG= t:BG(t=t)=(S 1BG) G^{ad} \sslash G = \sum_{t : B G}(t = t) = (S^1 \to BG)

    by the universal property of the circle as a HIT.

    Looking at (1) and (2) from above in HoTT, we see that (1) holds if we take (b) as a definition: Suppose Γ:BGGrp\Gamma : B G \to \infty Grp is an \infty-group with a GG-action, represented by BΓ:BGU *B \Gamma : B G \to U_*, taking values in pointed connected types. Then BΓG= t:BGBΓ t=B(GΓ)B \Gamma \sslash G = \sum_{t : B G} B \Gamma^t = B(G \ltimes \Gamma) is again pointed and connected, and the loop type is Ω(BΓG)= g:G(trp BΓg*=*)=G×Γ\Omega(B \Gamma \sslash G) = \sum_{g : G} (trp^{B \Gamma}\,g\,* = *) = G \times \Gamma, since we have a family of pointed types, so the transport of the point stays in place. (This represents the semi-direct product as you note.) We should be a bit careful, though, since the homotopy orbits of the type of elements of Γ\Gamma gives something different: ΓG= t:BGΓ t= t:BG(*= BΓ t*)\Gamma \sslash G = \sum_{t : B G} \Gamma^t = \sum_{t : B G} (* =_{B \Gamma^t} *).

    As to (2): this is exactly right, as a simple calculation shows (which I’ll skip here).

    Finally, the claim that Groups(H /BG)Groups(\mathbf{H}_{/\mathbf{B}G}) consists precisely of the above is clear from the HoTT point of view: If H\mathbf{H} is a model of HoTT, then so is H /BG\mathbf{H}_{/\mathbf{B}G} for any \infty-group GG in H\mathbf{H}, by simply prepending x:BGx : B G to the context of all judgments. In particular, we interpret “pointed connected type” as a family of pointed connected types indexed by BGB G, which is what Γ\Gamma was above.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJul 10th 2021
    • (edited Jul 10th 2021)


    …just note that…

    Maybe you could add that to the entry, under “Proof – In homotopy type theory” ?

    • CommentRowNumber23.
    • CommentAuthorUlrik
    • CommentTimeJul 10th 2021

    Will do, first thing tomorrow, as it’s getting late here.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJul 10th 2021

    On those points (1) and (2):

    Thanks again. I’ll think about that tomorrow, as I am about to call it quits, too. Are you saying I have a mistake in (1)? Will think about it.

    • CommentRowNumber25.
    • CommentAuthorUlrik
    • CommentTimeJul 10th 2021
    • (edited Jul 10th 2021)

    Not a mistake per se, it’s just that taking colimits in the type of groups doesn’t commute with taking elements, of course, but the notation can obscure that when we reuse the symbol for a group to denote its elements as well.

    • CommentRowNumber26.
    • CommentAuthorperezl.alonso
    • CommentTimeApr 15th 2024

    pointer (especially Part I):

    diff, v46, current