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.
I created a stub for stabilizer subgroup as it was needed by orbit.
This could do with a nPOV section, but I am not sure what to say for that. (I am still not sure how to ‘do’ an nPOV version of all the stuff around group actions. I would love to have it clear in my head as then a straightforward nPOV adaption of Grothendieck in SGA1 would be feasible. The treatment of SGA1 in the nLab still has some holes in it… e.g. the transition from the prorepresenting $P$ to the profinite group $Aut(P)$. I hope to sketch a bit more detail there soon. In fact a lot of the detail is skated over in the original SGA1. Any thoughts anyone?)
This could do with a nPOV section
I have added it here.
Hm, the server went down briefly after my edit.
So here is roughly what I typed: a group action $\rho : G \times X \to X$ is equivalently encoded in the corresponding action groupoid, which is the $\rho$-associated bundle to the the universal $G$-bundle $X \to X//G \to \mathbf{B}G$. The stabilizer group of an element $x : * \to X$ is the first homotopy group of $X//G$ at this point. Or, what is equivalent for 1-groups, it is the loop space object $\Omega_{x} X//G$.
(Hm, of course also the formulas don’t all display as long as the nLab server is down…)
In this last formulation the notion directly generalizes to stabilizer $\infty$-groups of $\infty$-group actions. And all of this goes through for cohesive $\infty$-groups, too.
This is also in section 2.3.7 here. (Which of course is, however, also not available as long as the server is down.)
Is there any need to revisit this thread, e.g., Mike’s suggestion?
While stabilizer group, isotropy group, isotropy subgroup, stabilizer subgroup and small group are also used, I think that the modern default is the shortest: just stabilizer. The latter term subsumes also the categorified versions.
Is there any need to revisit this thread, e.g., Mike’s suggestion?
Okay, sure. I had forgotten about this.
First, over there is discussed the stabilizer of a general morphism $Y \to X$, whereas I was here talking about stabilizers of global elements $* \to X$ only.
Second, there the action in $n$-categories is at least alluded to, whereas what I wrote here is for $(n,1)$-categories.
So there is room to generalize.
What I don’t see right now is how Mike’s suggestion gives a group object, in general. What Mike defines one can think of as producing the homotopy fixed point data fibered over the group (over each element $g$ of the group the data that makes $Y \to X$ a homotopy fixed point under $g$.) How is that a group object?
(I am genuinely asking, I don’t see it right now.)
First, over there is discussed the stabilizer of a general morphism $Y \to X$, whereas I was here talking about stabilizers of global elements $* \to X$ only.
Of course the definition of stabilizer $\infty$-groups as here immediately generalizes to this case:
for $G$ an action on $X$, and $Y$ any other object, there is an induced action on the internal hom $[Y, X]$ leading to an action $\infty$-groupoid $[Y,X]//G$. So now for given $f : Y \to X$ we can form the stabilizer $\infty$-group $\Omega_f ( [Y,X]//G )$.
edit:
as action $\infty$-groupoids we obtain $[Y,X]//G \to \mathbf{B}G$ from $X//G \to \mathbf{B}G$ as the $\infty$-pullback
$\array{ [Y,X]//G &\to& [Y, X//G] \\ \downarrow && \downarrow \\ \mathbf{B}G &\to& [Y,\mathbf{B}G] } \,,$where the bottom morphism picks the trivial cocycle and its global automorphisms (meaning that $G$ acts by the same element on all points of $Y$ at once, as it should). So the bottom morphism is the hom-adjunct to the projection $Y \times \mathbf{B}G \to \mathbf{B}G$.
Finally, I should say, for the definition that I was looking at, that and how there is a canonical morphism from the stabilizer $\infty$-group to the $\infty$-group $G$. It’s given by the top left morphism $i_x$ in the pasting diagram of homotopy pullbacks
$\array{ Stab_G(x) &\stackrel{i_x}{\to}& G &\to& * \\ \downarrow && \downarrow && \downarrow^{\mathrlap{x}} \\ * &\stackrel{x}{\to}& X &\to& X//G \\ && \downarrow && \downarrow^{\rho} \\ && * &\to& \mathbf{B}G } \,.$edit:
what is maybe noteworthy here is that this is just producing the long fiber sequence for the case where we regard $X$ and $X//G$ as objects pointed by $x$. So $i_x$ here is simply the looping of the representation itself:
$i_x \simeq \Omega_x \rho \,.$I believe the two definitions are actually the same, both in the case of global points and of arbitrary morphisms $Y\to X$. I actually found it easiest to prove this using HoTT, although quite possibly there is an easy arrow-theoretic proof too.
Note that the following code uses some lemmas and tactics from my fork of the HoTT repository that I haven’t gotten around to merging back into the main trunk yet.
Require Import Homotopy.
Let’s assume a pointed type $B G$, with the group object $G$ defined as its loop space.
Hypothesis BG : Type.
Hypothesis pt : BG.
Definition G := pt == pt.
Section OfAPoint.
Similarly, let’s assume the action groupoid as a fibration $X\sslash G \to B G$, with the type $X$ defined as its fiber over the basepoint. Note that the action of $G$ on $X$ is then via transport
.
Hypothesis XG : BG -> Type.
Let X := XG pt.
Let’s consider first the stabilizer of a point of $X$.
Hypothesis x : X.
Urs’s definition of the stabilizer of a point $x\colon X$ is as the loop space of that point, regarded as living in the total space $X\sslash G$ rather than in $X$.
Definition Urs_stab_pt : Type
:= (existT XG pt x) == (existT XG pt x).
On the other hand, my definition specializes to the following.
Definition Mike_stab_pt : Type
:= { g : G & transport g x == x }.
And their equivalence is just a special case of the characterization of path-spaces of total spaces.
Definition stab_pt_equiv : Urs_stab_pt <~> Mike_stab_pt
:= total_paths_equiv BG XG (existT XG pt x) (existT XG pt x).
End OfAPoint.
Section OfAMap.
Now let’s consider the stabilizer of a map $f\colon Y\to X$. Again we assume $X$ via its action groupoid.
Hypothesis XG : BG -> Type.
Let X := XG pt.
Hypothesis Y : Type.
Hypothesis f : Y -> X.
The following definition is the fibration $[Y, X\sslash G] \to [Y, BG]$.
Let Y_XG : (Y -> BG) -> Type
:= fun h => (forall y:Y, XG (h y)).
As a sanity check, we verify that its total space is, in fact, the function space $[Y, X\sslash G]$.
Lemma Y_XG_total : (Y -> sigT XG) <~> sigT Y_XG.
Proof.
apply section_total_equiv.
Defined.
Now this is the action groupoid $[Y,X]\sslash G$, defined with a pullback as in comment #7 above.
Let YX_G : BG -> Type
:= fun bg => Y_XG (fun _ => bg).
Urs’s definition of the stabilizer of $f\colon Y\to X$ is its stabilizer as a point of this action of $G$ on $[Y,X]$.
Definition Urs_stab_map : Type
:= Urs_stab_pt YX_G f.
Whereas here’s what my definition would give.
Definition Mike_stab_map : Type
:= { g : G & (transport g) o f == f }.
In this case, the proof of equivalence is a little longer, but it really only has two steps. First, we apply the characterization of path-spaces of total spaces to identify Urs’s definition with the total space of some fibration over $G$.
Definition stab_map_equiv : Urs_stab_map <~> Mike_stab_map.
Proof.
apply @equiv_compose with
(B := { g : G & transport (P := fun bg => Y -> XG bg) g f == f }).
refine (total_paths_equiv BG YX_G _ _).
Now we just need to show that this fibration (g
$\mapsto$ transport g f == f
) is fiberwise equivalent to g
$\mapsto$ transport g
$\circ$ f == f
, and for this it suffices to show that transport g f
is equivalent to (transport g)
$\circ$ f
.
assert (H : forall g:G,
transport (P := fun bg => Y -> XG bg) g f == (transport g) o f).
This should probably be a lemma in the standard library, but I don’t think it’s there yet, so we can just prove it here.
intros g; apply funext; intros y.
path_change ((fun h => h y)
(transport (P := fun bg => Y -> XG bg) g f)).
path_change (transport g ((fun h => h y) f)).
refine (trans_map _ (fun bg (h: Y -> XG bg) => h y) _).
Now we can complete the proof.
apply total_equiv with
(g := fun g => concat (!H g)).
intros g; apply concat_is_equiv_left.
Defined.
End OfAMap.
By the way, I think that $X\sslash G$ (iTex \sslash
) looks much nicer than $X//G$.
It saddens me that I find #9 almost completely unreadable.
I believe the two definitions are actually the same, […] I actually found it easiest to prove this using HoTT,
Mike, that is quite impressive. I literally have to run now, but thanks for this.
And thanks for
\sslash
I didn’t know that code and didn’t bother to search for it.
I can not read sslash in firefox on XP.
Zoran: That’s weird; I presume you have all the usual fonts installed. Can someone who knows more than I do suggest any reason why Zoran’s fonts might be missing that character?
I have the same problem as Zoran. And, while I’m thinking of it, $\preceq$ doesn’t render for me either. (That’s \preceq, in case it doesn’t render for you either.)
Todd, are you also in Firefox on Windows? Does it look okay in other browsers, or if you change the itex mode on the forum?
Thanks for asking, Mike. Yes, I nomally use Firefox on Windows XP. The \preceq, but not the \sslash, shows up in IE 8.0.6001.18702. (There might be something I need to enable which would allow me to see \sslash?) Sorry, I don’t know what it means to change itex mode, unless you mean to change the filter for formatting comments (?).
I have briefly added some of the above stuff to stabilizer group (not yet Mike’s stuff, though). Maybe I’ll add more later. But now I need to be taking care of something else.
I usually see all the fonts in $n$Lab and $n$Forum, sslash is one of rare exception, and example preceq from 15 as well.
@Todd: Go to “Account” at the top of the nForum page. On the left, click “change iTex mode”, select different things and see how it looks. This changes whether math is displayed as images or as MathML (which the browser has to understand — currently Firefox is the only major browser that supports MathML, so the “auto” setting selects MathML if you’re using Firefox and images otherwise. I think).
You can also test whether math is currently displaying as MathML or as images by trying to select part, but not all, of a mathematical formula with the cursor. This is possible with MathML, but not with an image.
1 to 20 of 20