module Algebra.Group.Instances.Dihedral where

# Dihedral groupsπ

The group of symmetries of a
regular
$n-gon,$
comprising rotations around the center and reflections, is called the
**dihedral group** of order
$2n:$
there are
$n$
rotations and
$n$
reflections, where each reflection can be obtained by composing a
rotation with a chosen reflection.

There are two notational conventions for the dihedral group
associated with the regular
$n-gon:$
the *geometric* convention is to write
$D_{n},$
while the *algebraic* convention is to write
$D_{2n},$
alluding to the order of the group. We will use the geometric convention
here.

Given any abelian
group
$G,$
we define the **generalised dihedral group**
$Dih(G)$
as the semidirect
product^{1} group
$Z/2ZβG,$
where the cyclic
group
$Z/2Z$
acts on
$G$
by `negation`

.

Dih : β {β} β Abelian-group β β Group β Dih G = Semidirect-product (LiftGroup _ (β€/ 2)) (AbelianβGroup G) $ β€/-out 2 (F-map-iso AbβͺGrp (negation G)) (ext Ξ» _ β inv-inv) where open Abelian-group-on (G .snd)

We can then define the dihedral group
$D_{n}$
as the generalised dihedral group of
$Z/nZ,$
the group of *rotations* of the regular
$n-gon.$

D : Nat β Group lzero D n = Dih (β€-ab/ n)

We also define the **infinite dihedral group**
$D_{β}$
as the generalised dihedral group of the group
of integers,
$Dih(Z).$

Dβ : Group lzero Dβ = Dih β€-ab

Geometrically, $D_{β}$ is the symmetry group of the following infinitely repeating frieze pattern, also known as $p1m1:$ there is a horizontal translation for every integer, as well as a reflection across the vertical axis that flips all the translations.

Note that our construction of $D_{n}$ makes $D_{0}$ equal to $D_{β},$ since $Z/0Z$ is $Z.$

Dββ‘Dβ : D 0 β‘ Dβ Dββ‘Dβ = ap Dih β€-ab/0β‘β€-ab