open import Algebra.Group.Cat.Base open import Algebra.Prelude open import Algebra.Group open import Cat.Instances.Delooping import Cat.Functor.Reasoning as Functor-kit module Algebra.Group.Action where

# Group actionsπ

A useful way to think about groups
is to think of their elements as encoding βsymmetriesβ of a particular
object. For a concrete example, consider the group
$(\bb{R}, +, 0)$
of real numbers under addition, and consider the unit circle^{1} sitting in
$\bb{C}$.
Given a real number
$x : \bb{R}$,
we can consider the βactionβ on the circle defined by

$a \mapsto e^{ix}a\text{,}$

which βvisuallyβ has the effect of rotating the point $a$ so it lands $x$ radians around the circle, in the counterclockwise direction. Each $x$-radian rotation has an inverse, given by rotation $x$ radians in the clockwise direction; but observe that this is the same as rotating $-x$ degrees counterclockwise. Addiitonally, observe that rotating by zero radians does nothing to the circle.

We say that
$\bb{R}$
*acts* on the circle by counterclockwise rotation; What this
means is that to each element
$x : \bb{R}$,
we assign a map
$\bb{C} \to \bb{C}$
in a way *compatible* with the group structure: Additive inverses
βtranslate toβ inverse maps, addition translates to function
composition, and the additive identity is mapped to the identity
function. Note that since
$\bb{C}$
is a set, this is equivalently a group homomorphism

$\bb{R} \to \id{Sym}(\bb{C})\text{,}$

where the codomain is the group of symmetries of $\bb{C}$. But what if we want a group $G$ to act on an object $X$ of a more general category, rather than an object of $\sets$?

## Automorphism groupsπ

The answer is that, for an object
$X$
of some category
$\ca{C}$,
the collection of all isomorphisms
$X \cong X$
forms a group under composition, generalising the construction of
$\id{Sym}(X)$
to objects beyond sets! We give refer to a βself-isomorphismβ as an
**automorphism**, and denote their group by
$\id{Aut}(X)$.

module _ {o β} (C : Precategory o β) where private module C = Cat C Aut : C.Ob β Group _ Aut X = (X C.β X) , to-group-on mg where mg : make-group (X C.β X) mg .make-group.group-is-set = C.β -is-set mg .make-group.unit = C.id-iso mg .make-group.mul g f = f C.βIso g mg .make-group.inv = C._Isoβ»ΒΉ mg .make-group.assoc x y z = C.β -pathp refl refl (sym (C.assoc _ _ _)) mg .make-group.invl x = C.β -pathp refl refl (x .C.invr) mg .make-group.invr x = C.β -pathp refl refl (x .C.invl) mg .make-group.idl x = C.β -pathp refl refl (C.idl _)

Suppose we have a category
$\ca{C}$,
an object
$X : \ca{C}$,
and a group
$G$;
A
**$G$-action
on
$X$**
is a group homomorphism
$G \to \id{Aut}(X)$.

Action : Group β β C.Ob β Type _ Action G X = Groups.Hom G (Aut X)

# As functorsπ

Recall that we defined the delooping of a monoid $M$ into a category as the category $\bf{B}M$ with a single object $\bull$, and $\hom(\bull, \bull) = M$. If we instead deloop a group $G$ into a group $\bf{B}G$, then functors $F : \bf{B}G \to \ca{C}$ correspond precisely to actions of $G$ on the object $F(\bull)$!

Functorβaction : {G : Group β} (F : Functor (B (Group-on.underlying-monoid (G .snd) .snd)) C) β Action G (F .Fβ tt) Functorβaction {G = G} F .fst it = C.make-iso (F .Fβ it) (F .Fβ (it β»ΒΉ)) (F.annihilate inverser) (F.annihilate inversel) where open Group-on (G .snd) module F = Functor-kit F Functorβaction F .snd .Group-hom.pres-β x y = C.β -pathp refl refl (F .F-β _ _) Actionβfunctor : {G : Group β} {X : C.Ob} (A : Action G X) β Functor (B (Group-on.underlying-monoid (G .snd) .snd)) C Actionβfunctor {X = X} A .Fβ _ = X Actionβfunctor A .Fβ e = A .fst e .C.to Actionβfunctor A .F-id = ap C.to (Group-hom.pres-id (A .snd)) Actionβfunctor A .F-β f g = ap C.to (Group-hom.pres-β (A .snd) _ _)