module Algebra.Group.Semidirect {β} where

# Semidirect products of groupsπ

Given a group
$A$
acting on another
group
$B$
(that is, equipped with a group homomorphism
$Ο:AβAut(B)$
from
$A$
to the automorphism
group of
$B),$
we define the **semidirect product**
$AβB$
as a variant of the direct
product
$AΓB$
in which the
$A$
component influences the multiplication of the
$B$
component.

To motivate the concept, letβs consider some examples:

- The dihedral group of order $2n,$ $D_{n},$ which is the group of symmetries of a regular $n-gon,$ can be defined as the semidirect product $Z/2ZβZ/nZ,$ where the action of $Z/2Z$ sends $1$ to the negation automorphism of $Z/nZ.$ Intuitively, a symmetry of the regular $n-gon$ has two components: a reflection (captured by the cyclic group $Z/2Z)$ and a rotation (captured by the cyclic group $Z/nZ);$ but when combining two symmetries, a reflection will swap the direction of further rotations. This is exactly captured by the semidirect product.
- The group of isometries of the square lattice $Z_{2}$ (considered as a subspace of $R_{2}),$ which we will refer to by its IUC notation $p4m,$ consists of reflections, rotations and translations. It can thus be defined as a further semidirect product of the dihedral group $D_{4}$ acting on the group of translations $Z_{2}$ in the obvious way.
- Leaving the discrete world, the group of all isometries of the plane
$R_{2}$
can be seen analogously as the semidirect product of the orthogonal
group
$O(2)$
acting on the translation group
$R_{2},$
where
$O(2)$
is itself the semidirect product of
$Z/2Z$
acting on the
*special*orthogonal group $SO(2),$ also known as the circle group.

module _ (A : Group β) (B : Group β) (Ο : Action (Groups β) A B) where private module A = Group-on (A .snd) module B = Group-on (B .snd)

We are now ready to define $AβB.$ The underlying set is the cartesian product $AΓB;$ the unit is the pair of units $(1_{A},1_{B}).$ The interesting part of the definition is the multiplication: we set $(a,b)β(a_{β²},b_{β²})=(aβ_{A}a_{β²},Ο_{a_{β²}}(b)β_{B}b_{β²}).$

Since our group
actions are *right* actions, what we define here is the
*right* semidirect product. The version that works with
*left* actions instead would be
$(aβ_{A}a_{β²},bβ_{B}Ο_{a}(b_{β²})).$

Semidirect-product : Group β Semidirect-product = to-group AβB where AβB : make-group (β A β Γ β B β) AβB .group-is-set = hlevel 2 AβB .unit = A.unit , B.unit AβB .mul (a , b) (a' , b') = a A.β a' , (Ο # a' # b) B.β b'

The definition of the inverses is then forced, and we easily check that the group axioms are verified.

AβB .inv (a , b) = a A.β»ΒΉ , (Ο # (a A.β»ΒΉ) # b) B.β»ΒΉ AβB .assoc (ax , bx) (ay , by) (az , bz) = Ξ£-pathp A.associative $ β Ο # (ay A.β az) # bx β B.β Ο # az # by B.β bz β‘β¨ ap! (unext (Ο .preserves .pres-β _ _) _) β©β‘ Ο # az # (Ο # ay # bx) B.β Ο # az # by B.β bz β‘β¨ B.associative β©β‘ (Ο # az # (Ο # ay # bx) B.β Ο # az # by) B.β bz β‘Λβ¨ ap (B._β bz) ((Ο # az) .Groups.to .preserves .pres-β _ _) β©β‘Λ Ο # az # (Ο # ay # bx B.β by) B.β bz β AβB .invl (a , b) = Ξ£-pathp A.inversel $ Ο # a # β (Ο # (a A.β»ΒΉ) # b) B.β»ΒΉ β B.β b β‘Λβ¨ apΒ‘ (pres-inv ((Ο # _) .Groups.to .preserves)) β©β‘Λ Ο # a # (Ο # (a A.β»ΒΉ) # (b B.β»ΒΉ)) B.β b β‘Λβ¨ ap (B._β b) (unext (pres-β (Ο .preserves) _ _) _) β©β‘Λ Ο # β a A.β»ΒΉ A.β a β # (b B.β»ΒΉ) B.β b β‘β¨ ap! A.inversel β©β‘ Ο # A.unit # (b B.β»ΒΉ) B.β b β‘β¨ ap (B._β b) (unext (pres-id (Ο .preserves)) _) β©β‘ b B.β»ΒΉ B.β b β‘β¨ B.inversel β©β‘ B.unit β AβB .idl (a , b) = Ξ£-pathp A.idl $ Ο # a # B.unit B.β b β‘β¨ ap (B._β b) (pres-id ((Ο # a) .Groups.to .preserves)) β©β‘ B.unit B.β b β‘β¨ B.idl β©β‘ b β

The natural projection from $AβB$ to the first component $A$ is a group homomorphism, but the same cannot be said about the second component (can you see why?).

β-proj : Groups.Hom Semidirect-product A β-proj .hom = fst β-proj .preserves .pres-β _ _ = refl

When the action of $A$ on $B$ is trivial, i.e.Β $Ο_{a}$ is the identity automorphism for all $a:A,$ itβs easy to see that the semidirect product $AβB$ agrees with the direct product $AΓB.$

module _ (A : Group β) (B : Group β) where private module A = Group-on (A .snd) module B = Group-on (B .snd)

Semidirect-trivial : Semidirect-product A B (trivial-action A B) β‘ Direct-product A B Semidirect-trivial = β«-Path (total-hom (Ξ» x β x) (record { pres-β = Ξ» _ _ β refl })) id-equiv

Another way to understand the semidirect product is to look at its definition for concrete groups, which is remarkably simple.