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

open import Cat.Prelude

open is-group-hom
open make-group

module Algebra.Group.Semidirect {β} where


# Semidirect products of groupsπ

Given a group acting on another group (that is, equipped with a group homomorphism from to the automorphism group of we define the semidirect product as a variant of the direct product in which the component influences the multiplication of the component.

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

• The dihedral group of order which is the group of symmetries of a regular can be defined as the semidirect product where the action of sends to the negation automorphism of Intuitively, a symmetry of the regular has two components: a reflection (captured by the cyclic group and a rotation (captured by the cyclic group 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 (considered as a subspace of which we will refer to by its IUC notation consists of reflections, rotations and translations. It can thus be defined as a further semidirect product of the dihedral group acting on the group of translations in the obvious way.
• Leaving the discrete world, the group of all isometries of the plane can be seen analogously as the semidirect product of the orthogonal group acting on the translation group where is itself the semidirect product of acting on the special orthogonal group 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 The underlying set is the cartesian product the unit is the pair of units The interesting part of the definition is the multiplication: we set

Note

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

  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 to the first component 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 on is trivial, i.e.Β  is the identity automorphism for all itβs easy to see that the semidirect product agrees with the direct product

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.