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

a↦eixa, a \mapsto e^{ix}a\text{,}

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

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

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

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

Automorphism groupsπŸ”—

The answer is that, for an object XX of some category C\ca{C}, the collection of all isomorphisms Xβ‰…XX \cong X forms a group under composition, generalising the construction of Sym(X)\id{Sym}(X) to objects beyond sets! We give refer to a β€œself-isomorphism” as an automorphism, and denote their group by Aut(X)\id{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 = C.β‰…-is-set
    mg .make-group.unit =
    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 (C.assoc _ _ _)
    mg .make-group.invl x = C.β‰…-pathp refl refl (x .C.invl)
    mg .make-group.invr x = C.β‰…-pathp refl refl (x .C.invr)
    mg .make-group.idl x = C.β‰…-pathp refl refl (C.idr _)

Suppose we have a category C\ca{C}, an object X:CX : \ca{C}, and a group GG; A GG-action on XX is a group homomorphism G→Aut(X)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 MM into a category as the category BM\bf{B}M with a single object βˆ™\bull, and Hom(βˆ™,βˆ™)=M\hom(\bull, \bull) = M. If we instead deloop a group GG into a group BG\bf{B}G, then functors F:BGβ†’CF : \bf{B}G \to \ca{C} correspond precisely to actions of GG on the object F(βˆ™)F(\bull)!

    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)
        open Group-on (G .snd)
        module F = Functor-kit F
    Functorβ†’action F .preserves .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)
    Action→functor A .F-id = ap (Group-hom.pres-id (A .preserves))
    Actionβ†’functor A .F-∘ f g = ap (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 β€œXX with a GG-action” for any particular XX, we take the total space of C\ca{C}-objects equipped with GG-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 → Group-hom-is-prop) _ _)
      .is-iso.linv x β†’ Functor-path (Ξ» _ β†’ refl) Ξ» _ β†’ refl

  1. this is not the higher inductive type S1S^1, but rather the usual definition of the circle as a subset of C\ca{C}.β†©οΈŽ