regular action



Representation theory

Group Theory



An action

*:G×XX * \;\colon\; G \times X \to X

of a group GG on a set XX is called regular if it is both transitive and free, that is, if for any pair of elements x,yXx,y \in X, there is exactly one group element gGg \in G such that g*x=yg * x = y.



Suppose GG acts transitively on XX by *:G×XX* : G \times X \to X, and suppose moreover that this action is faithful. Then GG acts freely (and hence regularly) on XX if and only if the group Aut G(X)Aut_G(X) of GG-equivariant automorphisms (i.e., bijections ϕ:XX\phi : X \to X commuting with the action of GG) acts transitively (and hence regularly) on XX.


First we show that Aut G(X)Aut_G(X) acts freely on XX. Suppose ϕAut G(X)\phi \in Aut_G(X) is such that ϕ(x)=x\phi(x) = x for some xXx\in X, and let yXy\in X be arbitrary. By the assumption that GG acts transitively, there is a gGg \in G such that y=g*xy = g*x. But then GG-equivariance implies that

ϕ(y)=ϕ(g*x)=g*ϕ(x)=g*x=y.\phi(y) = \phi(g*x) = g*\phi(x) = g*x = y.

Since this holds for all yYy\in Y, ϕ\phi must be equal to the identity ϕ=id X\phi = id_X, and therefore Aut G(X)Aut_G(X) acts freely on XX.

Next, suppose that GG also acts freely on XX, and let x,yXx,y \in X be arbitrary. Then we can define a GG-equivariant automorphism ϕ\phi such that ϕ(x)=y\phi(x) = y by

ϕ=zg z*y,\phi = z \mapsto g_z*y,

where for each zz, g zg_z is the unique group element such that z=g z*xz = g_z*x. Conversely, suppose that Aut G(X)Aut_G(X) acts transitively on XX, and let xXx\in X, gGg\in G such that g*x=xg*x = x. By the assumption, for any yXy \in X, there exists ϕAut G(X)\phi \in Aut_G(X) such that ϕ(x)=y\phi(x) = y, from which it follows that

g*y=g*ϕ(x)=ϕ(g*x)=ϕ(x)=y.g*y = g*\phi(x) = \phi(g*x) = \phi(x) = y.

Since g*y=yg*y = y for all yXy \in X, therefore g=1g = 1 by the assumption that GG acts faithfully on XX.


  • The action of GG on itself by multiplication :G×GG\cdot : G \times G \to G (on the left or on the right) is a regular action, called the (left or right) regular representation of GG.

  • If one views a combinatorial map MM as the transitive action of a certain group of permutations, then MM represents a regular map (Siran 2006) just in case this action is regular. For example, the five Platonic solids may be represented as regular combinatorial maps.

In homotopy type theory

We discuss regular actions via homotopy type theory.

Since doing group representation theory in homotopy type theory corresponds to working in the context of a delooped group in homotopy type theory, the regularity of an action is naturally expressed there. Transitivity ensures that all the points in the homotopy quotient are connected by equivalences, while freeness means that the space of equivalences between two points is itself contractible. Hence if *:BGX(*):Type\ast \colon \mathbf{B} G \vdash X(\ast): Type corresponds to a regular action, then the quotient *:BGX(*)\sum_{\ast: \mathbf{B} G} X(\ast) is contractible.

Restriction to 1-groups is unnecessary here, and we say


An ∞-action of an ∞-group is a regular \infty-action if its homotopy quotient is contractible.

For any GG-action (∞-action) X:BGUX \colon BG \to U, its automorphism group is (see at automorphism ∞-group in HoTT)

BAut G(X) (P:BGU)P=X B Aut_G(X) \coloneqq \sum_{(P:BG \to U)} \|P=X\|


X˜:BAut G(X)U \tilde{X} \colon B Aut_G(X) \to U

by X˜(P,)P(*)\tilde{X}(P,-) \coloneqq P(\ast).


If XX is regular, then X˜\tilde{X} is regular.


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

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

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

α:P=Xtrans(α)(p 0)=x. \sum_{\alpha : P = X} \mathrm{trans}(\alpha)(p_0) = x \,.

This type is equivalent to showing that there are

K: b:BGP(b)X(b)andK(*,p 0)=x 0. K : \prod_{b:BG} P(b) \simeq X(b) \;\;\;\; \text{and} \;\;\;\;\; K(*,p_0) = x_0 \,.

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

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

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


If XX is a principal homogeneous space on GG, in the sense that the type (g:G)g *(x)=y\sum_{(g:G)} g_\ast(x)=y is contractible for all x,y:X(*)x,y:X(\ast), and X˜\tilde{X} is regular, then XX is regular.


Again, we first show that X(*)X(\ast) is merely inhabited. The total space of X˜\tilde{X} has center of contraction (P,p 0)(P,p_0). Since P=X\|P=X\| and since we are proving a mere proposition, we get to use P=XP=X. Now X(*)\|X(\ast)\| follows from p 0:P(*)p_0:P(\ast). The regularity of XX is a mere proposition, so we get to use x 0:X(*)x_0:X(\ast). This gives us the center of contraction (*,x 0)(\ast,x_0). It remains to show that

(b:BG) (x:X(b)) (α:b=*)trans(α,x)=x 0\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

(b:BG) (x:X(b))isContr( (α:b=*)trans(α,x)=x 0)\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 BGBG is connected. Therefore it suffices to show that

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

This holds by assumption.


  • Jozef Siran, “Regular Maps on a Given Surface: A Survey”, Topics in Discrete Mathematics, 2006. (pdf)

  • Group Properties Wiki: Regular group action.

Last revised on April 24, 2018 at 09:16:55. See the history of this page for a list of all contributions to it.