open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Solver
open import Algebra.Group

open import Cat.Instances.Delooping
open import Cat.Instances.Functor
open import Cat.Instances.Sets
open import Cat.Diagram.Zero
open import Cat.Prelude

import Cat.Functor.Reasoning as Functor-kit
import Cat.Reasoning as Cat

module Algebra.Group.Action where

open is-group-hom
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 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 $\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 record where
      from (x , act) = Action→functor act
      linv x = Functor-path (λ _ → refl) λ _ → refl
      rinv x = Σ-pathp refl $
        total-hom-pathp _ _ _ (funext (λ i → C.≅-pathp _ _ refl))
          (is-prop→pathp (λ i → is-group-hom-is-prop) _ _)

Examples of actions🔗

module _ {o ℓ} {C : Precategory o ℓ} (G : Group ℓ) where
  trivial-action : ∀ X → Action C G X
  trivial-action X = Zero.zero→ ∅ᴳ

module _ {ℓ} (G : Group ℓ) where
  private module G = Group-on (G .snd)

  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