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

open Functor


# 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 $(\mathbb{R}, +, 0)$ of real numbers under addition, and consider the unit circle1 sitting in $\mathbb{C}$. Given a real number $x : \mathbb{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. Additionally, observe that rotating by zero radians does nothing to the circle.

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

$\mathbb{R} \to \mathrm{Sym}(\mathbb{C})\text{,}$

where the codomain is the group of symmetries of $\mathbb{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 $\mathbf{Sets}$?

## Automorphism groupsπ

The answer is that, for an object $X$ of some category $\mathcal{C}$, the collection of all isomorphisms $X \cong X$ forms a group under composition, generalising the construction of $\mathrm{Sym}(X)$ to objects beyond sets! We refer to a βself-isomorphismβ as an automorphism, and denote their group by $\mathrm{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 = C.β-is-set
mg .make-group.unit = C.id-iso
mg .make-group.mul g f = g C.βIso f
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.invl)
mg .make-group.idl x = C.β-pathp refl refl (C.idr _)


Suppose we have a category $\mathcal{C}$, an object $X : \mathcal{C}$, and a group $G$; A $G$-action on $X$ is a group homomorphism $G \to \mathrm{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 $\mathbf{B}M$ with a single object $\bull$, and $\mathbf{Hom}(\bull, \bull) = M$. If we instead deloop a group $G$ into a group $\mathbf{B}G$, then functors $F : \mathbf{B}G \to \mathcal{C}$ correspond precisely to actions of $G$ on the object $F(\bull)$!

  module _ {G : Group β} where
private BG = B (Group-on.underlying-monoid (G .snd) .snd) ^op

    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 = C.β-pathp refl refl (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 $\mathcal{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


1. this is not the higher inductive type $S^1$, but rather the usual definition of the circle as a subset of $\mathbb{C}$.β©οΈ