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 circle¹ sitting in $\mathbb{C}\text{.}$ Given a real number $x:\mathbb{R}\text{,}$ 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\text{-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}\text{,}$ 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

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

Automorphism groups🔗

The answer is that, for an object $X$ of some category $\mathcal{C}\text{,}$ 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)\text{.}$

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 
    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 = 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 $\mathcal{C}\text{,}$ an object $X:\mathcal{C}\text{,}$ and a group $G\text{;}$ A $G\text{-action}$ on $X$ is a group homomorphism $G\to \mathrm{Aut}(X)\text{.}$

  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 $\bullet \text{,}$ and $\mathbf{Hom}(\bullet ,\bullet )=M\text{.}$ If we instead deloop a group $G$ into a group $\mathbf{B}G\text{,}$ then functors $F:\mathbf{B}G\to \mathcal{C}$ correspond precisely to actions of $G$ on the object $F(\bullet )\text{!}$

  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 = 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\text{-action}$” for any particular $X\text{,}$ we take the total space of $\mathcal{C}\text{-objects}$ equipped with $G\text{-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