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 -radian 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 = 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 , an object , and a group ; A -action on is a group homomorphism .
Action : Group β β C.Ob β Type _ Action G X = Groups.Hom G (Aut X)
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 = 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 β with a -actionβ for any particular , we take the total space of -objects equipped with -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
this is not the higher inductive type , but rather the usual definition of the circle as a subset of .β©οΈ