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 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.
Is there a way to express this in HoTT, given a dependent type
$\ast: \mathbf{B} G \vdash X(\ast): Type ?$Oh, is it just that the dependent sum is contractible.
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”) .
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$?
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 }$I added the HoTT version of regularity.
Presumably then one can speak of the regularity of an infinity-action.
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$.
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.
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.
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.
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?
Yes please!
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.
Any other candidates for the HoTT treatment? Burnside’s lemma?
Maybe too 1-group-like, but there may be generalisable components of the proof.
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
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.
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?
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)$.
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.
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.
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?
1 to 24 of 24