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.
started an entry infinity-action
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:BG⊢V(c):Type an ∞-action we have
the dependent product
⊢∏c:BGV(c):Type
is the type of invariants of the action;
the dependent sum
⊢∑c:BGV(c):Type
is the quotient of the action
And hence for V1 and V2 two actions we have that
⊢∏c:BGV1(c)→V2(c):Type
is the type of G-homomorphisms (of G-equivariant maps);
⊢∑c:BGV1(c)→V2(c):Type
is the quotient of all maps by the G-cojugation action.
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.
added to infinity-action under a new section References – For discrete geometry pointers to articles that discuss GAct∞≃∞Grpd/BG.
(copied the same also to the end of the citations at principal infinity-bundle).
…
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 G-actions for G a topological group in the sense of G-spaces in equivariant homotopy theory (and hence with G not regarded as the geometrically discrete ∞-group of its underying homotopy type ) are equivalently objects in the slice (∞,1)-topos over BG is Elmendorf’s theorem together with the fact, highlighted in this context in
that
GSpace≃PSh∞(OrbG)≃PSh∞(Orb/BG)≃PSh∞(Orb)/BGis therefore the slice of the ∞-topos over the slice of the global orbit category over BG.
!include equivariant homotopy theory – table
See at equivariant homotopy theory for more references along these lines.
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)
There is a nice formalization of linearization of ∞-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.)
I have now written this (linearization of ∞-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 H action on 𝔤/𝔥 .
(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.)
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.
added publication data to:
added publication data to:
cross-linked the example of the adjoint action (here) with free loop space of a classifying space
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.
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≃ΩBG. 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.
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.
If a type in H/BG is a G ∞-action, what’s a dependent type there, so *:BG,v:V(*)⊢W(*,v):Type? Does that amount to a kind of equivariant bundle?
So if W is a principal bundle over V, then if all is in the context of BG that’s why the Γ at equivariant principal bundle needs to be considered with a G-action?
Yes, absolutely. I had tried to have a discussion on this in a thread elsewhere.
So for G any ∞-group, a “G-equivariant ∞-group” Γ should be a group-object in the slice H/BG. I still don’t quite understand these in full generality, but I understand the following sub-class:
Claim:
1) If Γ is a group in H which is equipped with a G-action by group automorphisms, then (a) Γ⫽G∈Groups(H/BG) and (b) B(Γ⫽G)≃(BΓ)⫽G.
2) The G-equivariant ∞-groups of this form are equivalent to split ∞-group extensions in H of the form Γhofib⟶Γ⋊G→G, under the identification (BΓ)⫽G≃B(Γ⋊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 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.
In any case, once we have such a group object in the slice over BG, then the ∞-groupoid of G-equivariant Γ-principal ∞-bundles on G-stacks X∈H/BG is
GEquvΓPrinBdls(H)X=H/BG(X⫽G,B(Γ⫽G))For the cases in the class (1), (2), this subsumes the traditional notion of equivariant principal bundles, under the embedding DTopologicalSpacesCDfflg↪H≔SmoothGroupoids∞.
Presumably whatever HoTT delivers is right, so then it’s a question of interpreting any HoTT-reasoning in whatever (∞,1)-topos. E.g., if we have the abstract general theory of Γ-principal bundles, then we just see what this amounts to in H/BG.
So that’s the issue with (1) and (2), whether these are the correct externalization of principal bundle theory internal to a (∞,1)-topos of the kind H/BG?
Hmm, what makes for externalization to be a non-trivial problem?
So (1) and (2) is certainly correct, in that they do yield a sub-∞-groupoid of Groups(H/BG) and they do subsume the traditional external equivariant groups and equivariant bundles.
I just don’t know if they exhaust Groups(H/BG). Hence I don’t know currently whether a “G-equivariant ∞-group” could be slightly more general than being a semidirect product ∞-group Γ⋊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)for ∞-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 ∞-bundles could show a new structural phenomenon not seen in equivariant topological bundles. It feels like this is unlikely, though.
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 Gad⫽G=LBG, just note that
Gad⫽G=∑t:BG(t=t)=(S1→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 Γ:BG→∞Grp is an ∞-group with a G-action, represented by BΓ:BG→U*, taking values in pointed connected types. Then BΓ⫽G=∑t:BGBΓt=B(G⋉Γ) is again pointed and connected, and the loop type is Ω(BΓ⫽G)=∑g:G(trpBΓg*=*)=G×Γ, 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 Γ gives something different: Γ⫽G=∑t:BGΓt=∑t:BG(*=BΓ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) consists precisely of the above is clear from the HoTT point of view: If H is a model of HoTT, then so is H/BG for any ∞-group G in H, by simply prepending x:BG to the context of all judgments. In particular, we interpret “pointed connected type” as a family of pointed connected types indexed by BG, which is what Γ was above.
Thanks!
…just note that…
Maybe you could add that to the entry, under “Proof – In homotopy type theory” ?
Will do, first thing tomorrow, as it’s getting late here.
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.
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.
pointer (especially Part I):
1 to 26 of 26