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
$(R,+,0)$
of real numbers under addition, and consider the unit circle^{1} sitting in
$C.$
Given a real number
$x:R,$
we can consider the βactionβ on the circle defined by

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. Additionally, observe that rotating by zero radians does nothing to the circle.

We say that
$R$
*acts* on the circle by counterclockwise rotation; What this
means is that to each element
$x:R,$
we assign a map
$Cβ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
$C$
is a set, this is equivalently a group homomorphism

where the codomain is the group of symmetries of $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
$C,$
the collection of all isomorphisms
$XβX$
forms a group under composition, generalising the construction of
$Sym(X)$
to objects beyond sets! We refer to a βself-isomorphismβ as an
**automorphism**, and denote their group by
$Aut(X).$

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

Suppose we have a category
$C,$
an object
$X:C,$
and a group
$G;$
A
**$G-action$
on
$X$**
is a group homomorphism
$GβAut(X).$

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

Since weβve defined
$fβg=gβf$
in the automorphism group, our definition corresponds to *right*
actions. If we had defined
$fβg=fβg$
instead, we would get *left* actions. Of course, the two
definitions are formally dual, so it does not really matter.

# As functorsπ

Recall that we defined the delooping of a monoid $M$ into a category as the category $BM$ with a single object $β,$ and $Hom(β,β)=M.$ If we instead deloop a group $G$ into a group $BG,$ then functors $F:BGβC$ correspond precisely to actions of $G$ on the object $F(β)!$

Functorβaction : (F : Functor BG C) β Action G (F .Fβ tt) Functorβaction F .hom it = C.make-iso (F .Fβ it) (F .Fβ (it β»ΒΉ)) (F.annihilate inversel) (F.annihilate inverser) where open Group-on (G .snd) module F = Functor-kit F Functorβaction F .preserves .is-group-hom.pres-β x y = ext (F .F-β _ _) Actionβfunctor : {X : C.Ob} (A : Action G X) β Functor BG C Actionβfunctor {X = X} A .Fβ _ = X Actionβfunctor A .Fβ e = (A # e) .C.to Actionβfunctor A .F-id = ap C.to (is-group-hom.pres-id (A .preserves)) Actionβfunctor A .F-β f g = ap C.to (is-group-hom.pres-β (A .preserves) _ _)

After constructing these functions in either direction, itβs easy
enough to show that they are inverse equivalences, but we must be
careful about the codomain: rather than taking
β$X$
with a
$G-action$β
for any particular
$X,$
we take the *total space* of
$C-objects$
equipped with
$G-actions.$

After this small correction, the proof is almost definitional: after
applying the right helpers for pushing paths inwards, weβre left with
`refl`

at all the leaves.

Functorβaction : is-equiv {B = Ξ£ _ (Action G)} Ξ» i β _ , Functorβaction i Functorβaction = is-isoβis-equiv Ξ» where .is-iso.inv (x , act) β Actionβfunctor act .is-iso.rinv x β Ξ£-pathp refl $ total-hom-pathp _ _ _ (funext (Ξ» i β C.β -pathp _ _ refl)) (is-propβpathp (Ξ» i β is-group-hom-is-prop) _ _) .is-iso.linv x β Functor-path (Ξ» _ β refl) Ξ» _ β refl

# Examples of actionsπ

For any group
$G,$
category
$C$
and object
$X:C,$
we have the **trivial action** of
$G$
on
$X$
which maps every element to the identity automorphism. It can be defined
simply as the zero
morphism
$GβAut(X).$

module _ {o β} {C : Precategory o β} (G : Group β) where trivial-action : β X β Action C G X trivial-action X = Zero.zeroβ β α΄³

Any group
$G$
acts on itself on the right in two ways: first,
$G$
acts on its underlying set by multiplication on the right. This is
sometimes called the **principal action** or the
**(right-)regular action**, and is the basis for Cayleyβs
theorem.

principal-action : Action (Sets β) G (G .fst) principal-action .hom x = equivβiso ((G._β x) , G.β-equivr x) principal-action .preserves .pres-β x y = ext Ξ» z β G.associative

$G$
also acts on itself *as a group* by **conjugation**.
An automorphism of
$G$
that arises from conjugation with an element of
$G$
is called an **inner automorphism**.

conjugation-action : Action (Groups β) G G conjugation-action .hom x = total-iso ((Ξ» y β x G.β»ΒΉ G.β y G.β x) , β-is-equiv (G.β-equivr x) (G.β-equivl (x G.β»ΒΉ))) (record { pres-β = Ξ» y z β group! G }) conjugation-action .preserves .pres-β x y = ext Ξ» z β group! G