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 of real numbers under addition, and consider the unit circle1 sitting in Given a real number we can consider the β€œaction” on the circle defined by

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

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

where the codomain is the group of symmetries of But what if we want a group to act on an object of a more general category, rather than an object of

Automorphism groupsπŸ”—

The answer is that, for an object of some category the collection of all isomorphisms forms a group under composition, generalising the construction of to objects beyond sets! We refer to a β€œself-isomorphism” as an automorphism, and denote their group by

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 an object and a group A on is a group homomorphism

  Action : Group β„“ β†’ C.Ob β†’ Type _
  Action G X = Groups.Hom G (Aut X)
Note

Since we’ve defined in the automorphism group, our definition corresponds to right actions. If we had defined 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 into a category as the category with a single object and If we instead deloop a group into a group then functors correspond precisely to actions of on the object

    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 β€œ with a ” for any particular we take the total space of equipped with

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 category and object we have the trivial action of on which maps every element to the identity automorphism. It can be defined simply as the zero morphism

module _ {o β„“} {C : Precategory o β„“} (G : Group β„“) where
  trivial-action : βˆ€ X β†’ Action C G X
  trivial-action X = Zero.zeroβ†’ βˆ…α΄³

Any group acts on itself on the right in two ways: first, 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

also acts on itself as a group by conjugation. An automorphism of that arises from conjugation with an element of 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

  1. this is not the higher inductive type , but rather the usual definition of the circle as a subset of β†©οΈŽ