If ($G$ is a group) and ($\rightcat X$ is a set), (a (right)
group action) is
(a function $\boxed{{\rightcat X} \times G \to \rightcat X}$) which is associative and unital,
meaning that $x(gh) = (xg)h$ and $xe = x$,
where $x\in \rightcat X$, $g,h\in G$ and $e$ is the unit (identity) element of $G$.
For (a left group action), just replace ${\rightcat X} \times G$ with $G \times {\rightcat X}$,
and change the equations to $(gh)x = g(hx)$ and $ex = x$.
For some important examples of group actions, see the post on
The bimodule of sets, functions and permutations.
<hr/>
For (given $G,\rightcat X$) in (a cartesian closed category), there are two other, equivalent, ways of (giving the structure) and (formulating the axioms), given as follows:
\[ \boxed{ \begin{array} {cccccccccc|clc|cccccccc|l} &&& {} \rlap{ \kern-2em \text{Structure} } &&&&&&& {} \rlap{ \kern8em \text{Description} } &&& {} \rlap{ \kern1.5em \text{Equational Axioms, aka Constraints} } &&&&&&&& {} \rlap{ \kern3em \text{Comment} } \\ &&& &&& &&& &&& && {} \rlap{ \kern-1em \text{Identity Axiom} } &&&& {} \rlap{ \kern-1.5em \text{Associativity Axiom} } \\ \hline {\rightcat X}_{-} & : & G & \to & [\rightcat X,\rightcat X] & : & g & \mapsto & {\rightcat X}_g &&& \text{the monoid $[\rightcat X,\rightcat X]$ as a $\textit{representation}$ of $G$} &&& {\rightcat X}_e & = & \rightcat{1_X} && {\rightcat X}_g{\rightcat X}_h & = & {\rightcat X}_{gh} & \rightcat X \text{ is functorial} \\ \hline {\rightcat -} \tensor {-} & : & {\rightcat X} \times G & \to & \rightcat X & : & \langle x,g \rangle & \mapsto & x \tensor g = xg &&& \text{$\rightcat X$ as a $\textit{module}$ over $G$, i.e. as a $G{-}\textit{module}$} &&& xe & = & x && (xg)h & = & x(gh) & \text{the action is associative} \\ &&&&&& [x]g & \mapsto & (x)g = xg &&& \text{Kelly's notation for actions of "clubs"} && &(x)e & = & x && \big((x)g\big)h & = & (x)(gh) \\ \hline \rightcat{ \widehat{ \black{(-)} } } & \rightcat : & \rightcat X & \rightcat\to & \rightcat{ [\black G, X] } & : & x & \rightcat\mapsto & \rightcat{ \hat{\black x} } &&& \text{the $G{-}\textit{orbits}$ of $\rightcat X$} : &&& e \rightcat{ \hat{\black x} } & = & x && h \rightcat{ \widehat{ \black{( g \rightcat{ \hat{\black x} } )} } } & = & (gh) \rightcat{ \hat{\black x} } \\ &&& &&& &&& && \boxed{ \rightcat{ {\hat{\black x}} : {\black G} \to X : {\black g} \mapsto {\black g} \rightcat{ \hat{\black x} } = {\black x}{\black g} = {\black x} X_{\black g} } } & &&& &&& \rightcat{ \hat{\black x} } {\rightcat X}_h & = & G_h \rightcat{ \hat{\black x} } & \text{each orbit $\rightcat{\hat{\black x}}$ is $G$-natural} \\ &&& &&& &&& && \rightcat{ \alpha : {\black G} \to X : {\black g} \mapsto {\black g}\alpha } \text{ such that } (\rightcat\alpha \text{ is } \mathit{natural}) & & & && && {\rightcat\alpha} {\rightcat X}_h & = & G_h {\rightcat\alpha} \\ \end{array} } \]
( The additional line for $[x]g \mapsto (x)g$ under "$\rightcat X$ as a $\textit{module}$") shows (a notation introduced by Kelly in (his papers on clubs) ).
Here of course ($g$ is being viewed as an operator), ($x$ as an operand).
In the event that $G$ has (a distinguished element $e$)
and (an internal composition operation, here denoted merely by juxtaposition),
often one is interested in (structures on the pair $\rightcat X,G$)
which are related to (the internal structure of $G$) by (the equations displayed in the panel at the right).
In the case where ($G$ is a group), this is what is meant by (the phrase "group action").
More generally, (structures satisfying such axioms) are called "algebras".
Precedent for denoting the action operation by $\tensor$ is in Section 3 of Im+Kelly.
<hr />
\[ \boxed{ \begin{array} {} && && && x, \gamma &&&& \gamma & \kern1em \\ && && && X \times_{\calC_0} \calC_1 & {} \rlap{\kern-1em \xrightarrow[\kern10em]{} } &&& \calC_1 \\ \gamma && \ast,\gamma && x,\gamma & \rightadj{ \nearrow \rlap{ \text{monic} } } && \rightadj{ \text{p.b.} } && \rightadj{ \nearrow \rlap{ \text{monic} } } \\ (c\downarrow \calC)_0 & \cong & 1 \times (c\downarrow \calC)_0 & \xrightarrow{\textstyle x \times 1} & X_c \times (c\downarrow \calC)_0 & {} \rlap{\kern-1em \xrightarrow[\kern10em]{} } &&& (c\downarrow \calC)_0 \\ && && && \leftcat{ \llap{\text{projection} \mapsto x} \Bigg\downarrow } \rightcat{ \Bigg\downarrow \rlap{ \text{action} \mapsto x\gamma = x X_\gamma} } &&&& \leftcat{ \llap{s} \Bigg\downarrow } \rightcat{ \Bigg\downarrow \rlap{t} } \\ && && && && & {} \rlap{ \kern-3em \leftcat{ \text{p.b. for } s } } \\ && \leftcat{ \llap{\text{projection} \mapsto \ast} \Bigg\downarrow } \phantom{ \rightcat{ \Bigg\downarrow } } && \leftcat{ \llap{\text{projection} \mapsto x} \Bigg\downarrow } \phantom{ \rightcat{ \Bigg\downarrow } } &&&& \leftcat{ \llap{s} \Bigg\downarrow } \phantom{ \rightcat{ \Bigg\downarrow \rlap{t} } } \\ && && && X & {} \rlap{\kern-1em \xrightarrow[\kern10em]{} } &&& \calC_0 \\ && && & \rightadj{ \nearrow \rlap{ \text{monic} } } && \rightadj{ \text{p.b.} } && \llap{\leftcat c} \rightadj{ \nearrow \rlap{ \text{monic} } } \\ && 1 & {} \rlap{ \kern-0.5em \xrightarrow[\textstyle x]{\kern3em} } & X_c & {} \rlap{\kern-1em \xrightarrow[\kern10em]{} } &&& 1 \\ && \ast & \mapsto & x \\ \end{array} } \]
Given $x \in \rightcat X$, let $c \in \calC_0$ be its image in $\calC_0$.
Then
(the map $\hat x : (c\downarrow \calC)_0 \to \rightcat X : \gamma \mapsto \gamma \hat x = x\gamma$ via the action of $\calC$ on $\rightcat X$)
is (the <i>orbit</i> of $x$ under the action).
Then the following are equivalent statements:
($\hat x$ is an equivariant map of right $\calC$-sets)
iff $x(\gamma\gamma') = (x\gamma)\gamma'$ for all compatible $x,\gamma,\gamma'$
iff (the associativity axiom holds for the action).
<hr />
Given $\rightcat{ \boxed{ \alpha : { \black{\hom c \calC -} } \Rightarrow X } }$,
a natural transformation from (the covariant regular representation of $\calC$ at $c$) to (an arbitrary covariant $\calC$-set $\rightcat X$),
we have, for each $d \in \calC$ and $f \in \hom c \calC d$,
\[ \boxed{ \begin{array} {} 1_c & && \rightcat\mapsto && (1_c)\alpha_c = \boxed{\check\alpha} \\ c && \hom c \calC c & \rightcat{ \xrightarrow[\kern3em]{ \textstyle {\black c} \alpha = \alpha_{\black c} } } & {\rightcat X}_c \\ \llap{f} \Bigg\downarrow && \llap{\hom c \calC f} \Bigg\downarrow & \rightcat{ {\black f} \alpha = \alpha_{\black f} } & \Bigg\downarrow \rlap{{\rightcat X}_f} \\ d && \hom c \calC d & \rightcat{ \xrightarrow[\textstyle {\black d} \alpha = \alpha_{\black d}]{\kern3em} } & {\rightcat X}_d \\ (1_c) \hom c \calC f = 1_c f = f & && \rightcat \mapsto && \begin{array}{} (1_c) \hom c \calC f {\rightcat\alpha}_d & \xlongequal{\textstyle (1_c){\rightcat\alpha}_f} & (1_c) {\rightcat\alpha}_c {\rightcat X}_f \\ \llap{ \text{defn } \hom c \calC f } \Vert && \Vert \rlap{ \text{defn } \check{\rightcat\alpha} \text{ -- restriction} } \\ (1_c f) {\rightcat\alpha}_d && {\check{\rightcat\alpha}} {\rightcat X}_f \\ \llap{ 1_c \text{ is an identity} } \Vert && \Vert \rlap{ \text{defn } {\hat{()}}_d \text{ -- extension} } \\ f \boxed{{\rightcat\alpha}_d} && f \boxed{ \big( \hat{ {\check{\rightcat\alpha}} } {\big)}_d } & \kern7em \\ \text{thus: } & \boxed{ \boxed{ \rightcat\alpha = \hat{\check{\rightcat\alpha}} } } \\ \end{array} \\ \end{array} } \]
On the other hand, given $x \in {\rightcat X}_c$,
\[ \check{ \hat x } \xlongequal{\textstyle \text{defn } \check{()} } 1_c \big(\hat x\big)_c \xlongequal{\textstyle \text{defn } \big(\hat x\big)_c } x {\rightcat X}_{1_c} \xlongequal{\textstyle {\rightcat X} \text{ preserves identities} } x \rightcat{ 1_{X_{\black c}} } = x \]
Thus $\boxed{ \check{ \hat x } = x }$.
Thus finally we have a bijection
\[ \boxed{ \leftcat{ (\check{\rightcat\alpha} = x) \in {\rightcat X}_c} \; { \leftadj{ \xrightarrow[\text{extension}]{\textstyle \hat{()} }} \atop { \rightadj{ \xleftarrow[\textstyle \check{()}]{\text{restriction}} } } } \; \rightcat{ { \hom {\hom c \calC -} {[\calC, \Set]} {\rightcat X} } \ni (\alpha = \hat {\leftcat x}) } } \]
almost surely the simplest and most basic example of the "Yoneda bijection".
<hr />
To prepare for generalizations, and to justify calling $\hat x$ an "extension",
consider the forgetful functor $\boxed{ \rightadj U \mathrel{\rightadj :} \rightcat{G{-}\Set} \mathrel{\rightadj\to} \leftcat\Set \mathrel{\rightadj :} \rightcat X \mathrel{\rightadj\mapsto} \rightcat X \rightadj U \mathrel{\rightadj =} \leftcat X }$,
where we have followed the common practice of using the same letter $X$ to denote both a $G$-set, with its action $X \times G \to X$, and its underlying mere set $\leftcat X$,
and where $\rightcat{G{-}\Set}$ denotes (the category of $G$-sets) (not to be confused with G-spots! :-).
$G$'s multiplication $\boxed{ G \times G \to G }$ makes $G$ a right (and also a left) $G$-set, the (right) (or left) regular representation of $G$.
The identity element $\boxed{e}$ of $G$ may be specified ("named") via an arrow in $\leftcat\Set$, $\boxed{ \leftadj{ e : \leftcat 1 \to G \rightadj U } }$.
The content of the most basic Yoneda bijection may then be expressed by the statement
\[ \boxed{ \leftadj { e : \leftcat 1 \to G \rightadj U \kern1em \text{ is a universal arrow from $\leftcat 1$ to $\rightadj U$.} } } \]
\[ \boxed{ \begin{array} {} && \leftadj G \\ & \leftadj{ \llap{e} \nearrow} & \Vert & \rightcat{ \searrow \rlap{ \exists! \, \hat{\leftcat x} = \alpha \text{ ; the } \textit{extension} \leftcat{\text{ of } x}} } \\ \leftcat 1 & \leftcat{ {} \rlap{ \kern-1em \xrightarrow[ {}\rlap{\textstyle \kern-3em \forall \, x = \check{\rightcat\alpha} \text{ ; the } \textit{restriction} \rightcat{\text{ of } \alpha}} ]{\kern8em} } } &&& \rightcat X & \kern10em \\ \end{array} } \]
Here the two arrows originating at the set $\leftcat 1$ are both arrows in $\leftcat\Set$, while the arrow $\rightcat{{\leftadj G} \to X}$ is in $\rightcat{G{-}\Set}$.
What "$\leftadj{ e : {\leftcat 1} \to G {\rightadj U} } \kern1em \text{ is a universal arrow from $\leftcat 1$ to $\rightadj U$}$" means is:
For every arrow $\leftcat{ 1 \xrightarrow[\kern1.5em]{\textstyle x} {\rightcat X} }$ as at bottom (i.e. for every element $\leftcat{x \in X}$),
there exists a unique morphism of $G$-sets $G \to \rightcat X$ as at right which makes the triangle commute.
We denote this unique morphism of $G$-sets, whose existence and uniqueness is guaranteed by the universal property, by $\boxed{ \hat x }$.
$\newcommand\GSet{{\rightcat{G{-}\Set}}}$
A familiar example, for $V$ a vector space over $\R$, and $v \in \rightcat V$ a vector in it:
\[ \begin{array} {} && \R \\ & \llap{1} \nearrow & \Vert & \searrow \rlap{ \hat v = \rightcat l \text{ ; the $\textit{extension}$ of $v$, the parameterized line through $v$}} \\ \leftcat 1 & {} \rlap{ \kern-1em \xrightarrow[\textstyle v = \check l \rlap{ \text{ ; the $\textit{restriction}$ of $\rightcat l$}}]{\kern10em} } &&& \rightcat V \\ \end{array} \]
Here of course "$1$" is being used to denote both a one-element set, say $\leftcat{1=\{\emptyset\}}$, and the real number usually so denoted.
<hr />
Returning to the more general $\rightcat{G{-}\Set}$ context,
the "bijection between arrows" formulation has a generalization to an adjunction:
Given a group $G$ in $\Set$, there is an adjunction:
\[ \boxed{ \leftcat{Y \in \Set} \; { { \leftadj{ \xrightarrow[\kern6em]{\textstyle (-\times G)} } } \atop { \rightadj{ \xleftarrow[\textstyle U]{\kern6em} } } } \; \rightcat{G{-}\Set \ni X} } \]
I.e. the arrows in the box above are functors and we have a natural (in $\leftcat Y$ and $\rightcat X$) bijection of sets
\[ \boxed{ \begin{array} {} \rightcat\alpha & \rightcat\in & \rightcat{ \hom { \leftadj{ ({\leftcat Y} \times G) } } {(G{-}\Set)} X } \\ && \red{\wr\Vert} \\ \leftcat{ x } & \leftcat\in & \leftcat{ \hom Y \Set {\rightcat X \rightadj U} } \\ \end{array} } \]
We can depict the relation between $\leftcat x$ and $\rightcat\alpha$ with:
\[ \boxed{ \begin{array} {} && \leftadj{ {\leftcat Y} \times G } \\ & \leftadj{ \llap{ \leftcat Y \times e } \nearrow } & \Vert & \rightcat{ \searrow \rlap{ \exists! \, \hat {\leftcat x} = \alpha \text{ ; the $\textit{extension}$ of $\leftcat x$} }} \\ \leftcat{ Y \cong Y\times 1 } & {} \rlap{ \kern-1em \leftcat{ \xrightarrow[\textstyle \forall \, x = \check{\rightcat\alpha} \rlap{ \text{ ; the $\textit{restriction}$ of $\rightcat\alpha$}}]{\kern11em} } } &&& \rightcat X & \kern10em \\ \end{array} } \]
$\leftadj{ {\leftcat Y} \times G }$ is the free $\rightcat{ G{-}\Set}$ on the set $\leftcat Y$;
the unit (just a function) is $\leftadj{ \leftcat Y \times e }$.
The counit, a morphism of $\leftadj G$-algebras, at a $\rightcat{ G{-}\Set \; X }$ is just the $\leftadj G$-action $\leftadj{ {\rightcat X \rightadj U} \times G } \mathrel{\rightadj\to} \rightcat X $.
The above relations may be perspicaciously viewed be embedding them in the 2-category $\CAT$ of large 1-categories.
\[ \boxed{ \begin{array} {ccccccccc|l} &&&& \calC \calP^\ast &&&& \calC \calP^\ast & \text{Yoneda structure operation } \calP^\ast \text{ on } \calC \\ &&&& \rightcat\Vert &&&& \rightcat\Vert \\ &&&& [\calC, \Set] &&&& [\calC, \Set] & \text{discrete opfibrations (dof) on } \calC \\ &&&& \rightcat\Vert &&&& \rightcat\Vert \\ &&&& [\leftadj G \mathbf B, \Set] &&&& [\leftadj G \mathbf B, \Set] & \text{discrete opfibrations (dof) on } \leftadj G \mathbf B \\ &&&& \rightcat\Vert &&&& \rightcat\Vert \\ \I & {} \rlap{ \kern-1em \rightcat{ \xrightarrow[\kern11em]{\textstyle X} } } &&& \GSet & {} \rlap{ \kern-2em \rightcat{ \xrightarrow[\kern11em]{} } } &&& \GSet \\ & \leftcat{ \llap Y \searrow } & \rightcat{ \raise1ex{ \smash{ \llap{\exists! \alpha} \Bigg\Uparrow } } } & \leftadj{ \nearrow \rlap{\scriptstyle \kern-3em ({\leftcat -} \times G)} } \leftcat{ \raise.3ex{ \smash{ \Bigg\Uparrow \rlap{ \forall x} } } } & \leftadj{ \raise0ex{ \smash{ \Bigg\Uparrow \rlap{\scriptstyle \kern-2em \eta = ({\leftcat -} \times e)} } } } & \rightadj{ \searrow \rlap{\kern-1em U} } & \rightadj{ \raise1ex{ \smash{ \Bigg\Uparrow \rlap{\scriptstyle \kern-2em \epsilon = \text{action}} } } } & \leftadj{ \nearrow \rlap{({\leftcat -} \times G)} } && \red{\text{the adjointness! :-)} } \\ && \leftcat\Set & {} \rlap{ \leftcat{ \kern-1em \xrightarrow{\kern13em} } } &&& \leftcat\Set \\ \end{array} } \]
The two adjunction triangle equalities are,
first, that for any set $\leftcat Y$, $\leftcat{ y \in Y}$, and $g \in G$,
\[ {\leftcat Y} \times {\leftadj G} \to {\leftcat Y} \times {\leftadj G} : [\leftcat y] \leftadj g \mathrel{\leftadj\mapsto} \big[ [\leftcat y] \leftadj e \big] \leftadj g \mathrel{\rightadj\mapsto} [\leftcat y] \leftadj{(e g)} \xlongequal{\text{left identity axiom for group } \leftadj G} [\leftcat y] \leftadj g \; , \]
and second, that for any $G$-set $\rightcat X$ and $x \in \rightcat X \rightadj U$,
\[ {\rightcat X \rightadj U} \to {\rightcat X \rightadj U} : x \mathrel{\leftadj\mapsto} [x] \leftadj e \mathrel{\rightadj\mapsto} (x) \leftadj e = x \leftadj e \xlongequal{\text{identity axiom for action of $\leftadj G$ on $X$}} x \; . \]
Note that $\hat{\leftcat x}$ equals
\[ \begin{array}{} \leftadj{ {\leftcat Y} \times G } & \xrightarrow[\kern3em]{\leftadj{ \leftcat x \times G }} & \leftadj{ {\rightcat X \rightadj U} \times G } & \rightadj{ \xrightarrow[\kern3em]{\rightcat X \rightadj \epsilon} } & \rightcat X \\ [\leftcat y] \leftadj g & \mapsto & [\leftcat {yx}] \leftadj g & \mapsto & (\leftcat {yx}) \leftadj g \end{array} \]
<hr />
Here are 2-D, 1-D, and 0-D diagrams for the above situation:
\[ \boxed{ \begin{array} {rcc} {} \rlap{ \kern-21em \text{The Element/Orbit Bijection $\boxed{\leftadj\eta \leftrightarrow \rightcat\alpha}$ (i.e., the Yoneda Lemma) for a Representation $\rightcat X$ of a Group $G$} } \\ \hline \\ \text{viewing $\CAT$ as a double category (trivial vertical 1-cells)} && \boxed{ \begin{array} {} \leftcat\calI & \leftadj{ \xrightarrow [\kern2em] {\textstyle e} } & \leftadj G & \rightcat{ \xrightarrow [\kern2em] {\textstyle X} } & \Set \\ \leftcat{\Big\vert} & \llap g \smash{\Bigg\Uparrow} & \leftadj{\Big\vert} & \rightcat{ \smash{\Bigg\Uparrow} \rlap{ \kern-1.9em \boxed{\alpha = \hat\eta} } } & \Big\vert \\ \leftcat\calI & \leftadj{ \xrightarrow [\kern2em] {\textstyle e} } & \llap{\smash{ {\ulcorner g \urcorner} \Bigg\Uparrow }} {\leftadj G} \rlap{\smash{ \leftadj{ \Bigg\Uparrow \boxed{\eta = \check\alpha} } }} & \leftadj{ \xrightarrow [\kern2em] {\textstyle \hom e G {\leftcat -}} } & \Set \\ \leftcat{\Big\vert} && \leftadj{ \llap{1_e} \Big\Uparrow } && \Big\vert \\ \leftcat\calI & \leftcat{ {} \rlap{ \kern-2em \xrightarrow [\textstyle 1] {\kern12em} } } &&& \Set \\ \end{array} } \\ \text{2-D, in the very large 2-category $\CAT$ of large 1-categories} & \kern2em & \boxed{ \begin{array} {} && \leftadj G & \leftadj{ \xlongequal{\kern1em} } & \leftadj G & \leftadj{ \xlongequal{\kern1em} } & \leftadj G \\ & \leftadj{ \llap{e} \nearrow} & \buildrel \textstyle g \over \Leftarrow & \leftadj{ \llap{e} \nearrow } \rlap{\smash{ \kern-1em \Bigg\Uparrow \rlap{ \ulcorner g \urcorner } }} & \smash{ \leftadj{ \llap{1_e} \Big\Uparrow \rlap{\smash{ \kern1.5em \Bigg\Uparrow \rlap{ \boxed\eta } }} } } & \leftadj{ \searrow \rlap{ \kern-2.3em \hom e G - } } & \rightcat{ \buildrel \textstyle {} \rlap{ \kern-1.6em \boxed{\alpha = \hat\eta} } \over \Rightarrow } & \rightcat{ \searrow \rlap X } \\ \leftcat\calI & \leftcat{ \xlongequal{\kern1em} } & \leftcat\calI & {} \rlap{ \kern-1.5em \leftcat{ \xrightarrow[\textstyle 1]{\kern9.5em} } } &&& \leftcat\Set & \leftcat{ \xlongequal{\kern1em} } & \leftcat\Set \\ \end{array} } \\ \\ \text{1-D, in the large category $\Set$ of small sets} && \boxed{ \begin{array} {} && X_e \\ & \rightcat{ \llap{ {\alpha}_{\black e} } \nearrow } && \rightcat{ \nwarrow \rlap{ X_{\black g} } } \\ \hom e G e && g{\rightcat\alpha} && {\rightcat X}_e & \\ & \llap{ \hom e G g } \nwarrow && \rightcat{ \nearrow \rlap{ \alpha_{\black e} } } \\ && \hom e G e \\ & \llap{ \ulcorner g \urcorner } \nwarrow & {\big\uparrow} \rlap{1_e} & \leftadj{ \nearrow \rlap{ \boxed{ \eta = \rightcat{\check\alpha} } } } \\ && 1 \\ \end{array} } \\ \\ \text{0-D, in the small set ${\rightcat X}_{\leftadj e}$ } && \boxed{ g{ \rightcat{ \alpha_{\black e} } } = {\leftadj\eta} g = \rightcat{\check\alpha} g = g \big( \rightcat{ \hat{\check\alpha} } {\big)}_e } \\ \end{array} } \]
<hr />
\[ \boxed{ \begin{array} {l|c|c} \text{action} & & \text{equalities in } \N & \text{bijections in } \Set \\ \hline \text{one object} & X \times G \to X & \text{orbit-stabilizer equation} ; \text{class equation}& \text{orbit-element bijection} \\ \hline \text{several objects} & X_c \times {\hom c \calC -} \to X_- & & \text{Yoneda lemma} \\ \end{array} } \]
<hr />
$ \leftadj{ \llap{ \text{(quotient map of ($\red{\hat x}$ cokernel))} } \nearrow } $
\[ \boxed{ \begin{array} {} \rightadj{ \boxed{ \text{Stab}_{\black x} = \text{Aut}_{\black x} } } & \rightadj\rightarrowtail & G & \leftadj{ \displaystyle \mathop\twoheadrightarrow^{\text{quotient}}_{\text{map}} } & \leftadj{ \boxed{ {\black G}{/}\rightadj{ \text{Stab} }_{\black x} } } \\ && \wr\Vert && \red{\wr\Vert} \rlap{ \; ( \leftadj{\text{orbit}} \text{-} \rightadj{\text{stabilizer}} \text{ theorem} ) } \\ \smash{\rightadj{\Bigg\downarrow}} & \smash{ \rightadj{ \raise5ex{\kern-4em \lrcorner} \text{p.b.} } } & 1 \times G & \leftadj{ \buildrel \textstyle \black{\hat x} \over \twoheadrightarrow } & \leftadj{ \boxed{ [\black x] = \black{xG} } } \rlap{ \kern0em \xrightarrow[\smash{\kern12em}]{\textstyle !} } && 1 & \kern0em \\ && \llap{ {\ulcorner x \urcorner} \times G } \Bigg\downarrow & \llap{ \scriptstyle \text{defn. } \red{\hat x} \kern-.6em } \smash{ \red{ \buildrel \textstyle \kern1em \boxed{\hat x} \over \searrow } } \rlap{ \scriptstyle \kern-.5em \text{image fact.} } & \Bigg\downarrow & \smash{ \rightadj{ \raise3ex{\kern-2em \lrcorner} \text{p.b.} } } & \Bigg\downarrow \rlap{ \ulcorner \leftadj{ [\black x] } \urcorner } \\ \rightadj{ \boxed{ \black{ (\displaystyle \mathop\rightrightarrows^\tensor_{\pi_X}) } \, \text{Equalizer} } } & \rightadj\rightarrowtail & X \times G & \displaystyle \mathop\rightrightarrows^\tensor_{\pi_X} & X {} \rlap{ \kern0em \leftadj{\xrightarrow{\kern5em}} } && \leftadj{ \boxed{ \black{ (\displaystyle \mathop\rightrightarrows^\tensor_{\pi_X}) } \, \text{Coeq} = \black X {/} \black G = (\black{X//G})\pi_0 } } \\ &&&& x & \leftadj\mapsto & {} \rlap{ \kern-4em \leftadj{ [\black x] } = xG = G\hat x = \hat x \, { \leftadj{ \text{Image} } } } \\ &&&& X {} \rlap{ \rightadj{ \xleftarrow[\textstyle a]{ \kern1em \text{section} \kern1em } } } && \leftadj{ \boxed{ \black{ (\displaystyle \mathop\rightrightarrows^\tensor_{\pi_X}) } \, \text{Coeq} = \black X {/} \black G = (\black{X//G})\pi_0 } } \\ \end{array} } \]
\[ \boxed{ \displaystyle X \buildrel \Gsets \over \cong \leftadj{ \sum_{[\black x] \in {\black X}/{\black G}} } \leftadj{ [\black x] } \buildrel \Gsets \over \cong \leftadj{ \sum_{ [\black x] \in {\black X}/{\black G}} } {\black G}{/}\rightadj{ \text{Stab} _{a_{\leftadj{[\black x]}}} } } \]
(E.g., let $G = \langle \{\pm1\}, \times, +1\rangle$. Then, with (the evident action given algebraically by multiplication or geometrically by reflection),
\[ \boxed{ X = \{-2,-1,0,1,2\} \cong \{\pm 2\} \leftadj+ \{\pm1\} \leftadj+ \{0\} = [2] \leftadj+ [1] \leftadj+ [0] \cong \{\pm1\}/\rightadj{\{+1\}} \leftadj+ \{\pm1\}/\rightadj{\{+1\}} \leftadj+ \{\pm1\}/\rightadj{\{\pm1\}} } \] To see a picture of this $\{\pm1\}$-set, visit https://golem.ph.utexas.edu/category/2021/07/diversity_and_the_mysteries_of.html )
The last general result yields, via $|\cdot| : \FinSet_0 \to \N$, (the "<a href="https://ncatlab.org/nlab/show/class+equation">class equation</a>", an equality of natural numbers in $\N$): \[ \boxed{ |X| = \Big|\sum_{[\black x] \in {\black X}/{\black G}} G/{ \rightadj{ \text{Stab} }_{\black x} } \Big| = \sum_{[\black x] \in {\black X}/{\black G}} |G/{ \rightadj{ \text{Stab} }_{\black x} }| = \sum_{[\black x] \in {\black X}/{\black G}} |G|/{ \rightadj{ |\text{Stab} }_{\black x} | } } \]
which is numerically equivalent to the equality of rational numbers in $\Q$: \[ \boxed{ |X|/|G| \buildrel \text{above} \over = \sum_{ [\black x] \in {\black X}/{\black G} } 1/{ \rightadj{ | \text{Stab} }_{\black x} | } \buildrel \text{defns} \over = \sum_{ [\black x] \in \pi_0({\black X}//{\black G}) } 1/| \Aut{x} | \buildrel \text{defn.} \over \equiv \boxed{ |X//G| } } \] , this last (the "<a href="https://ncatlab.org/nlab/show/groupoid+cardinality"><i>groupoid cardinality</i></a>" of the <a href="https://ncatlab.org/nlab/show/action+groupoid"><i>action groupoid</i></a> $\boxed{X//G}$ associated with (the action $X_-$)). Note the usage of (the full-up equality $\boxed{X/G = \pi_0(X//G)}$), and that (the groupoid cardinality) can be defined for (any groupoid), not just (action groupoids).
<hr />
<h3>References</h3>
Im+Kelly, A Universal Property of the Convolution Monoidal Structure
https://doi.org/10.1016/0022-4049(86)90005-8
For possible future use: $\rightadj{\text{counit of }} ( \leftadj{\text{cokernel}} \text{-} \rightadj{\text{kernel}} \text{ adjunction} ) \rightadj{\text{ is here monic}} ) }$
