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 an -action we have
the dependent product
is the type of invariants of the action;
the dependent sum
is the quotient of the action
And hence for and two actions we have that
is the type of -homomorphisms (of -equivariant maps);
is the quotient of all maps by the -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 .
(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 -actions for a topological group in the sense of G-spaces in equivariant homotopy theory (and hence with not regarded as the geometrically discrete ∞-group of its underying homotopy type ) are equivalently objects in the slice (∞,1)-topos over is Elmendorf’s theorem together with the fact, highlighted in this context in
that
is therefore the slice of the -topos over the slice of the global orbit category over .
!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 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 . 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 is a -action, what’s a dependent type there, so ? Does that amount to a kind of equivariant bundle?
So if is a principal bundle over , then if all is in the context of that’s why the at equivariant principal bundle needs to be considered with a -action?
Yes, absolutely. I had tried to have a discussion on this in a thread elsewhere.
So for any -group, a “-equivariant -group” should be a group-object in the slice . I still don’t quite understand these in full generality, but I understand the following sub-class:
Claim:
1) If is a group in which is equipped with a -action by group automorphisms, then (a) and (b) .
2) The -equivariant -groups of this form are equivalent to split -group extensions in of the form , under the identification .
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 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 .
In any case, once we have such a group object in the slice over , then the -groupoid of -equivariant -principal -bundles on -stacks is
For the cases in the class (1), (2), this subsumes the traditional notion of equivariant principal bundles, under the embedding .
Presumably whatever HoTT delivers is right, so then it’s a question of interpreting any HoTT-reasoning in whatever -topos. E.g., if we have the abstract general theory of -principal bundles, then we just see what this amounts to in .
So that’s the issue with (1) and (2), whether these are the correct externalization of principal bundle theory internal to a -topos of the kind ?
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 and they do subsume the traditional external equivariant groups and equivariant bundles.
I just don’t know if they exhaust . Hence I don’t know currently whether a “-equivariant -group” could be slightly more general than being a semidirect product -group . (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
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 , just note that
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 is an -group with a -action, represented by , taking values in pointed connected types. Then is again pointed and connected, and the loop type is , 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: .
As to (2): this is exactly right, as a simple calculation shows (which I’ll skip here).
Finally, the claim that consists precisely of the above is clear from the HoTT point of view: If is a model of HoTT, then so is for any -group in , by simply prepending to the context of all judgments. In particular, we interpret “pointed connected type” as a family of pointed connected types indexed by , 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