Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 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

1. • CommentRowNumber1.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexI created a short page: [[regular action]] (of a group). It mainly just contains the definition and a simple-minded proof that a faithful transitive action $* : G \times X \to X$ acts freely (and hence regularly) on $X$ if and only if the automorphism group $Aut_G(X)$ acts transitively (and hence regularly) on $X$. If anyone knows of a more abstract proof, please feel free (and hence regular) to insert it.

   I created a short page: regular action (of a group). It mainly just contains the definition and a simple-minded proof that a faithful transitive action $* : G \times X \to X$ acts freely (and hence regularly) on $X$ if and only if the automorphism group $Aut_G(X)$ acts transitively (and hence regularly) on $X$. If anyone knows of a more abstract proof, please feel free (and hence regular) to insert it.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks! I noticed that _[[action]]_ did not cross-link to any of the related entries, so I added some more pointers [here](https://ncatlab.org/nlab/show/action#RelatedConcepts).

   Thanks!

   I noticed that action did not cross-link to any of the related entries, so I added some more pointers here.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIs there a way to express this in HoTT, given a dependent type $$ \ast: \mathbf{B} G \vdash X(\ast): Type ? $$

   Is there a way to express this in HoTT, given a dependent type

   $$\ast: \mathbf{B} G \vdash X(\ast): Type ?$$
4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOh, is it just that the dependent sum is contractible.

   Oh, is it just that the dependent sum is contractible.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, that's one of the places where geometric homotopy theory beautifies traditional theory: the condition that an action be transitive and free together just means that its _homotopy quotient_ is contractible: transitivity ensures that all the points in the homotopy quotient are connected by equivalences, freeness means that the space of equivalences between two points is itselef contractible. (E.g. the homotopy quotient of a non-free action with stabilizer $G_x$ of some point $x$ remembers all the non-freedom by sending that point to $\mathbf{B}G_x$.) That in turn makes the theory of principal bundles in homotopy theory more beautiful than the classical theory: in geometric homotopy theory _every_ quotient map $P \to P/G$ is $G$-principal. (Here "geometric homotopy theory" = "$\infty$-topos") .

   Yes, that’s one of the places where geometric homotopy theory beautifies traditional theory: the condition that an action be transitive and free together just means that its homotopy quotient is contractible: transitivity ensures that all the points in the homotopy quotient are connected by equivalences, freeness means that the space of equivalences between two points is itselef contractible. (E.g. the homotopy quotient of a non-free action with stabilizer $G_x$ of some point $x$ remembers all the non-freedom by sending that point to $\mathbf{B}G_x$.)

   That in turn makes the theory of principal bundles in homotopy theory more beautiful than the classical theory: in geometric homotopy theory every quotient map $P \to P/G$ is $G$-principal.

   (Here “geometric homotopy theory” = “$\infty$-topos”) .

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMay 2nd 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSo can we prove the theorem Noam mentioned in HoTT? At least the direction that if $G$ acts regularly on $X$ then so does $Aut_G(X)$? How do we define $Aut_G(X)$? Maybe something like $$\mathbf{B}Aut_G(X) \coloneqq \sum_{P:\mathbf{B}G\to \mathcal{U}} \Vert P = X\Vert $$ ?

   So can we prove the theorem Noam mentioned in HoTT? At least the direction that if $G$ acts regularly on $X$ then so does $Aut_G(X)$? How do we define $Aut_G(X)$? Maybe something like

   $$\mathbf{B}Aut_G(X) \coloneqq \sum_{P:\mathbf{B}G\to \mathcal{U}} \Vert P = X\Vert$$

   ?

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeMay 2nd 2016
   • (edited May 2nd 2016)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThe key fact is that $Act_G(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G}$. A $G$-action on $X$ is a type in context $\mathbf{B}G$ with fiber $X$, hence a homotopy fiber sequence of the form $$ \array{ X &\longrightarrow& X/ G \\ && \downarrow \\ && \mathbf{B}G } \,. $$ A homomorphism of $G$-actions is just a function in context $\mathbf{B}G$. Hence $Aut_G(X)$ is just the automorphisms group formed in in context $\mathbf{B}G$ and then base changed (via dependent product) down to the empty context (or else to the ambient context $\Gamma$, of course). The action of $G$ on $X$ is regular if $X / G \simeq \ast$. From this, it is plausible that $Aut_G(X)$, whose elements are cells in the bottom of the following diagram, has regular action on $X$ precisely if $X/G \simeq \ast$ $$ \array{ X && \longrightarrow && X \\ \downarrow && && \downarrow \\ X/G && \longrightarrow && X/G \\ & \searrow && \swarrow \\ && \mathbf{B}G } $$

   The key fact is that $Act_G(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G}$.

   A $G$-action on $X$ is a type in context $\mathbf{B}G$ with fiber $X$, hence a homotopy fiber sequence of the form

   $$\array{ X &\longrightarrow& X/ G \\ && \downarrow \\ && \mathbf{B}G } \,.$$

   A homomorphism of $G$-actions is just a function in context $\mathbf{B}G$. Hence $Aut_G(X)$ is just the automorphisms group formed in in context $\mathbf{B}G$ and then base changed (via dependent product) down to the empty context (or else to the ambient context $\Gamma$, of course).

   The action of $G$ on $X$ is regular if $X / G \simeq \ast$.

   From this, it is plausible that $Aut_G(X)$, whose elements are cells in the bottom of the following diagram, has regular action on $X$ precisely if $X/G \simeq \ast$

   $$\array{ X && \longrightarrow && X \\ \downarrow && && \downarrow \\ X/G && \longrightarrow && X/G \\ & \searrow && \swarrow \\ && \mathbf{B}G }$$
8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 3rd 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI added the HoTT version of regularity. Presumably then one can speak of the regularity of an [[infinity-action]].

   I added the HoTT version of regularity.

   Presumably then one can speak of the regularity of an infinity-action.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeMay 3rd 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Presumably then one can speak of the regularity of an [[infinity-action]]. As I said, $G$ $\infty$-acts regularly on $X$ if the homotopy quotuent is contractible, $X/G\simeq \ast$.

   Presumably then one can speak of the regularity of an infinity-action.

   As I said, $G$ $\infty$-acts regularly on $X$ if the homotopy quotuent is contractible, $X/G\simeq \ast$.

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI guess I meant is that worth saying here. It's of course trivial in a sense, but then has 'regular $\infty$-action' ever appeared in print? Where did the term 'regular action' come from? Was it derived from 'regular representation'? I seem to remember from my undergraduate days that the regular representation of a finite group was quite a useful device containing all its irreducible representations. Is there then a regular $\infty$-representation of an $\infty$-group $G$, achieved through some kind of [linearization](https://ncatlab.org/nlab/show/infinity-action#Linearization) of $G$? But of course we have $\infty$-group $\infty$-rings at [[infinity-group of units]]. Ah, but that's only for abelian $\infty$-groups. Then there's all of [[infinity-representation]] and [[(infinity,1)-module bundle]]. But this is heading towards being a distraction. Still you'd think someone in the HoTT community could usefully look into such matters.

    I guess I meant is that worth saying here. It’s of course trivial in a sense, but then has ’regular $\infty$-action’ ever appeared in print?

    Where did the term ’regular action’ come from? Was it derived from ’regular representation’? I seem to remember from my undergraduate days that the regular representation of a finite group was quite a useful device containing all its irreducible representations.

    Is there then a regular $\infty$-representation of an $\infty$-group $G$, achieved through some kind of linearization of $G$?

    But of course we have $\infty$-group $\infty$-rings at infinity-group of units. Ah, but that’s only for abelian $\infty$-groups.

    Then there’s all of infinity-representation and (infinity,1)-module bundle. But this is heading towards being a distraction. Still you’d think someone in the HoTT community could usefully look into such matters.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2016
    • (edited May 3rd 2016)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Where did the term 'regular action' come from? I'd guess it derives from regularity of quotients, as in "regular point", etc.. But I don't know the history.

    Where did the term ’regular action’ come from?

    I’d guess it derives from regularity of quotients, as in “regular point”, etc.. But I don’t know the history.

12. • CommentRowNumber12.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: EgbertRijke
    Format: MarkdownItexHere are the claims with their proofs. Of course, in the email list, Mike finished the argument of the first claim. Let $BG$ be a pointed connected type with loop space $G$. Let $X : BG \to U$ be a type $X(\ast)$ with a $G$-action on it, and define $BAut_G(X) := \sum_{(P:BG \to U)} \|P=X\|$. Then we have $Y : BAut_G(X) \to U$ given by $Y(P,-) := P(\ast)$. *Claim 1. If $X$ is regular, then $Y$ is regular.* Proof. First, we need to argue that $X(\ast)$ is merely inhabited. Since $X$ is regular, we have $\sum_{(b:BG)} X(b)$ contractible. This gives a center of contraction $(b,x)$. Now, since $BG$ is connected, it follows that $\|b=\ast\|$. Since we are proving the mere proposition $\|X(\ast)\|$, we get to use $b=\ast$. Now we obtain $\|X(\ast)\|$ . Next, to show that $X$ is regular we need to show that $X$ has a contractible total space. The type $\sum_{(b : BAut_G(X))} Y(b)$ is equivalent to $\sum_{(P:BG \to U)} \|P=X\| \times P(\ast)$. Contractibility is a mere proposition, and we have $\|X(\ast)\|$, so we get to use a point $x:X(\ast)$. This gives us a center of contraction $(X,refl,x)$ of the total space of $Y$. Now let $P : BG \to U$, let $ \| P = X \|$, let $p_0 : P(\ast)$. To show regularity, it suffices to find a term of type $\sum_{\alpha : P = X} \mathrm{trans}(\alpha)(p_0) = x$ This type is equivalent to showing that there are $K : \prod_{b:BG} P(b) \simeq X(b)$, and $K(*,p_0) = x_0$ Now we use that $X(b)$ is equivalent to $b=\ast$ (we get this fact from regularity, together with a point $x:X(\ast)$). Since we need this particular fiberwise equivalence, it suffices to show that $\sum_{b:BG} P(b)$ is contractible. Now this is a mere proposition, so we can eliminate $t : \| P = X \|$ to obtain the proof. *Claim 2. If $X$ is a principal homogeneous space on $G$, in the sense that the type $\sum_{(g:G)} g_\ast(x)=y$ is contractible for all $x,y:X(\ast)$, and $Y$ is regular, then $X$ is regular.* Proof. Again, we first show that $X(\ast)$ is merely inhabited. The total space of $Y$ has center of contraction $(P,p_0)$. Since $\|P=X\|$ and since we are proving a mere proposition, we get to use $P=X$. Now $\|X\|$ follows from $p_0:P(\ast)$. The regularity of $X$ is a mere proposition, so we get to use $x_0:X(\ast)$. This gives us the center of contraction $(\ast,x_0)$. It remains to show that $\prod_{(b:BG)} \prod_{(x:X(b))} \sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0$. Of course, it would suffice to prove the stronger statement $\prod_{(b:BG)} \prod_{(x:X(b))} \mathrm{isContr} (\sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0)$. However, now we get to use that $BG$ is connected. Therefore it suffices to show that $\prod_{x:X(*)} isContr (\sum_{\alpha : G} \mathrm{trans}(\alpha,x) = x_0)$ This holds by assumption.

    Here are the claims with their proofs. Of course, in the email list, Mike finished the argument of the first claim.

    Let $BG$ be a pointed connected type with loop space $G$. Let $X : BG \to U$ be a type $X(\ast)$ with a $G$-action on it, and define $BAut_G(X) := \sum_{(P:BG \to U)} \|P=X\|$. Then we have $Y : BAut_G(X) \to U$ given by $Y(P,-) := P(\ast)$.

    Claim 1. If $X$ is regular, then $Y$ is regular.

    Proof. First, we need to argue that $X(\ast)$ is merely inhabited. Since $X$ is regular, we have $\sum_{(b:BG)} X(b)$ contractible. This gives a center of contraction $(b,x)$. Now, since $BG$ is connected, it follows that $\|b=\ast\|$. Since we are proving the mere proposition $\|X(\ast)\|$, we get to use $b=\ast$. Now we obtain $\|X(\ast)\|$ .

    Next, to show that $X$ is regular we need to show that $X$ has a contractible total space. The type $\sum_{(b : BAut_G(X))} Y(b)$ is equivalent to $\sum_{(P:BG \to U)} \|P=X\| \times P(\ast)$. Contractibility is a mere proposition, and we have $\|X(\ast)\|$, so we get to use a point $x:X(\ast)$. This gives us a center of contraction $(X,refl,x)$ of the total space of $Y$.

    Now let $P : BG \to U$, let $\| P = X \|$, let $p_0 : P(\ast)$. To show regularity, it suffices to find a term of type

    $\sum_{\alpha : P = X} \mathrm{trans}(\alpha)(p_0) = x$

    This type is equivalent to showing that there are

    $K : \prod_{b:BG} P(b) \simeq X(b)$, and $K(*,p_0) = x_0$

    Now we use that $X(b)$ is equivalent to $b=\ast$ (we get this fact from regularity, together with a point $x:X(\ast)$). Since we need this particular fiberwise equivalence, it suffices to show that

    $\sum_{b:BG} P(b)$

    is contractible. Now this is a mere proposition, so we can eliminate $t : \| P = X \|$ to obtain the proof.

    Claim 2. If $X$ is a principal homogeneous space on $G$, in the sense that the type $\sum_{(g:G)} g_\ast(x)=y$ is contractible for all $x,y:X(\ast)$, and $Y$ is regular, then $X$ is regular.

    Proof. Again, we first show that $X(\ast)$ is merely inhabited. The total space of $Y$ has center of contraction $(P,p_0)$. Since $\|P=X\|$ and since we are proving a mere proposition, we get to use $P=X$. Now $\|X\|$ follows from $p_0:P(\ast)$. The regularity of $X$ is a mere proposition, so we get to use $x_0:X(\ast)$. This gives us the center of contraction $(\ast,x_0)$. It remains to show that

    $\prod_{(b:BG)} \prod_{(x:X(b))} \sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0$.

    Of course, it would suffice to prove the stronger statement

    $\prod_{(b:BG)} \prod_{(x:X(b))} \mathrm{isContr} (\sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0)$.

    However, now we get to use that $BG$ is connected. Therefore it suffices to show that

    $\prod_{x:X(*)} isContr (\sum_{\alpha : G} \mathrm{trans}(\alpha,x) = x_0)$

    This holds by assumption.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Egbert, that's really nice. The idea would be that such stuff should go into the nLab entry, as there it is more usefully recorded. Might you have time to copy it over?

    Thanks, Egbert, that’s really nice.

    The idea would be that such stuff should go into the nLab entry, as there it is more usefully recorded. Might you have time to copy it over?

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes please!

    Yes please!

15. • CommentRowNumber15.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: EgbertRijke
    Format: MarkdownItexI've put it on the nLab page. As it is my first contribution to the nLab, please have a quick look to see whether it is okay.

    I’ve put it on the nLab page. As it is my first contribution to the nLab, please have a quick look to see whether it is okay.

16. • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 4th 2016
    • (edited May 4th 2016)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAny other candidates for the HoTT treatment? [Burnside's lemma](https://en.wikipedia.org/wiki/Burnside%27s_lemma)? Maybe too 1-group-like, but there may be generalisable components of the proof.

    Any other candidates for the HoTT treatment? Burnside’s lemma?

    Maybe too 1-group-like, but there may be generalisable components of the proof.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2016
    • (edited May 4th 2016)
    • PermaLink
    Author: Urs
    Format: MarkdownItexEgbert, thanks. That's impressive for a first $n$Lab edit. Hopefully you'll get the chance to do more such! I just went through your text, [here](https://ncatlab.org/nlab/show/regular+action#InHomotopyTypeTheory), and added a bunch of hyperlinks to keywords. Such as _[[mere proposition]]_, _[[inhabited type]]_, _[[contractible type]]_, etc. Also to _[automorphism infinity-group in HoTT](https://ncatlab.org/nlab/show/automorphism+infinity-group#InHomotopyTypeTheory)_

    Egbert, thanks. That’s impressive for a first $n$Lab edit. Hopefully you’ll get the chance to do more such!

    I just went through your text, here, and added a bunch of hyperlinks to keywords. Such as mere proposition, inhabited type, contractible type, etc. Also to automorphism infinity-group in HoTT

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, thanks! Burnside's lemma happens a special case of the [linearity of traces](http://arxiv.org/abs/1406.7854). Developing the latter in HoTT would be a good deal of work, but might pay off.

    Yes, thanks!

    Burnside’s lemma happens a special case of the linearity of traces. Developing the latter in HoTT would be a good deal of work, but might pay off.

19. • CommentRowNumber19.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016
    • PermaLink
    Author: EgbertRijke
    Format: MarkdownItexPossibly the condition of being a principal homogeneous space over $G$ can be weakened, because right now we only use the regularity of $\tilde{X}$ to conclude that $\|X(\ast)\|$. Any suggestions?

    Possibly the condition of being a principal homogeneous space over $G$ can be weakened, because right now we only use the regularity of $\tilde{X}$ to conclude that $\|X(\ast)\|$. Any suggestions?

20. • CommentRowNumber20.
    • CommentAuthorLuis_Scoccola
    • CommentTimeMay 6th 2016
    • PermaLink
    Author: Luis_Scoccola
    Format: MarkdownItex[Here](https://www.dropbox.com/s/8wvyun7lq3diyz3/infgrp.pdf?dl=0) I have some (**very** brief and informal) notes about infinity groups in HoTT. I'm sorry to share a link to a pdf but if some of the things written there make any sense I will write them down in an nLab entry. The notes include (potential) definitions for transitive actions, free actions and faithful actions, and some informal arguments to motivate them. I'm afraid I did not have the time to see if this definition of faithful action serves to generalize the lemma that started this thread, but I will think about it. Are these defintions reasonable or maybe already known? Also I have a question regarding infinity groups is HoTT. Is there a standard definition for infinity-subgroup, or for the kernel of an infinity-group morphism? I was thinking of maybe being able to prove some kind of Orbit-Stabilizer theorem. Remark: I used a computer-language-like notation for dependent sums and dependent products: a dependent sum is written $(a : A) \times P(a)$ and a dependent product $(a:A)\to P(a)$.

    Here I have some (very brief and informal) notes about infinity groups in HoTT. I’m sorry to share a link to a pdf but if some of the things written there make any sense I will write them down in an nLab entry. The notes include (potential) definitions for transitive actions, free actions and faithful actions, and some informal arguments to motivate them. I’m afraid I did not have the time to see if this definition of faithful action serves to generalize the lemma that started this thread, but I will think about it.

    Are these defintions reasonable or maybe already known? Also I have a question regarding infinity groups is HoTT. Is there a standard definition for infinity-subgroup, or for the kernel of an infinity-group morphism? I was thinking of maybe being able to prove some kind of Orbit-Stabilizer theorem.

    Remark: I used a computer-language-like notation for dependent sums and dependent products: a dependent sum is written $(a : A) \times P(a)$ and a dependent product $(a:A)\to P(a)$.

21. • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 7th 2016
    • (edited May 7th 2016)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIt would be great to have $\infty$-group theory written out somewhere in full HoTT style. Urs has written extensively on [[infinity-actions]]. Regarding a Orbit-Stabilizer theorem, the place to look, as I said on the [transitive action thread](https://nforum.ncatlab.org/discussion/7103/transactive-action/), is [[stabiliser group]]. There, sub-$\infty$-groups are being taken as monomorphisms: >in contrast to the classical situation, this morphism is not in general a monomorphism anymore, hence the stabilizer $Stab_\rho(x)$ is not a _sub_-group of $G$ in general. That tallies with why what's at [[normal+subgroup#NormalMorphismOfInfinityGroups]] is not called a normal sub-$\infinity$-group, which would need the extra mono condition. We should, but don't, have something on this at [[subgroup]]. [[infinity-group]] has other links, such as [[center of an infinity-group]].

    It would be great to have $\infty$-group theory written out somewhere in full HoTT style. Urs has written extensively on infinity-actions. Regarding a Orbit-Stabilizer theorem, the place to look, as I said on the transitive action thread, is stabiliser group.

    There, sub-$\infty$-groups are being taken as monomorphisms:

    in contrast to the classical situation, this morphism is not in general a monomorphism anymore, hence the stabilizer $Stab_\rho(x)$ is not a sub-group of $G$ in general.

    That tallies with why what’s at normal+subgroup#NormalMorphismOfInfinityGroups is not called a normal sub-$\infinity$-group, which would need the extra mono condition. We should, but don’t, have something on this at subgroup.

    infinity-group has other links, such as center of an infinity-group.

22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 7th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI have not read this, but it seems possibly relevant: [Sylow theorems for ∞-groups](http://arxiv.org/abs/1602.04494) > Viewing Kan complexes as ∞-groupoids implies that pointed and connected Kan complexes are to be viewed as ∞-groups. A fundamental question is then: to what extent can one "do group theory" with these objects? In this paper we develop a notion of a finite ∞-group: an ∞-group with finitely many non-trivial homotopy groups which are all finite. We prove a homotopical analog of the Sylow theorems for finite ∞-groups. We derive two corollaries: the first is a homotopical analog of the Burnside's fixed point lemma for p-groups and the second is a "group-theoretic" characterization of (finite) nilpotent spaces.

    I have not read this, but it seems possibly relevant: Sylow theorems for ∞-groups

    Viewing Kan complexes as ∞-groupoids implies that pointed and connected Kan complexes are to be viewed as ∞-groups. A fundamental question is then: to what extent can one “do group theory” with these objects? In this paper we develop a notion of a finite ∞-group: an ∞-group with finitely many non-trivial homotopy groups which are all finite. We prove a homotopical analog of the Sylow theorems for finite ∞-groups. We derive two corollaries: the first is a homotopical analog of the Burnside’s fixed point lemma for p-groups and the second is a “group-theoretic” characterization of (finite) nilpotent spaces.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 8th 2016
    • (edited Feb 20th 2018)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOne of the authors, [[Matan Prasma]] (used to be written Prezma), has worked on normal maps of $\infty$-groups, as it says at [[normal+subgroup#NormalMorphismOfInfinityGroups]]. In the general setting, for normal $f: K \to G$ there is a long fiber sequence $$ G\sslash K \to \mathbf{B}K \stackrel{\mathbf{B}f}{\to}\mathbf{B}G \to \mathbf{B}(G\sslash K) \,. $$ Does the normal sub-$\infty$-group case, where $f$ is a monomorphism, merit special attention, I wonder. A Jordan-Holder decomposition? How about the [isomorphism theorems](https://en.wikipedia.org/wiki/Isomorphism_theorem#Groups)?

    One of the authors, Matan Prasma (used to be written Prezma), has worked on normal maps of $\infty$-groups, as it says at normal+subgroup#NormalMorphismOfInfinityGroups. In the general setting, for normal $f: K \to G$ there is a long fiber sequence

    $$G\sslash K \to \mathbf{B}K \stackrel{\mathbf{B}f}{\to}\mathbf{B}G \to \mathbf{B}(G\sslash K) \,.$$

    Does the normal sub-$\infty$-group case, where $f$ is a monomorphism, merit special attention, I wonder. A Jordan-Holder decomposition?

    How about the isomorphism theorems?

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexmentioned definition via [[shear map]] isomorphism and made the equivalent notion of [[torsor]] more explicit. <a href="https://ncatlab.org/nlab/revision/diff/regular+action/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/regular+action/10">v10</a>, <a href="https://ncatlab.org/nlab/show/regular+action">current</a>

    mentioned definition via shear map isomorphism and made the equivalent notion of torsor more explicit.

    diff, v10, current