open import Algebra.Group.Instances.Integers
open import Algebra.Group.Instances.Cyclic
open import Algebra.Group.Semidirect
open import Algebra.Group.Cat.Base
open import Algebra.Group.Action
open import Algebra.Group.Ab

open import Cat.Functor.Base
open import Cat.Prelude

module Algebra.Group.Instances.Dihedral where

Dihedral groups🔗

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

Given any abelian group $G\text{,}$ we define the generalised dihedral group $\mathrm{Dih}(G)$ as the semidirect product¹ group $\mathbb{Z}/2\mathbb{Z}⋉G\text{,}$ where the cyclic group $\mathbb{Z}/2\mathbb{Z}$ acts on $G$ by negation.

Dih : ∀ {ℓ} → Abelian-group ℓ → Group ℓ
Dih G = Semidirect-product (LiftGroup _ (ℤ/ )) (Abelian→Group G) $
  ℤ/-out  (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 $\mathbb{Z}/n\mathbb{Z}\text{,}$ the group of rotations of the regular $n\text{-gon.}$

D : Nat → Group lzero
D n = Dih (ℤ-ab/ n)

We also define the infinite dihedral group $D_{\infty }$ as the generalised dihedral group of the group of integers, $\mathrm{Dih}(\mathbb{Z})\text{.}$

D∞ : Group lzero
D∞ = Dih ℤ-ab

Geometrically, $D_{\infty }$ is the symmetry group of the following infinitely repeating frieze pattern, also known as $p1m1\text{:}$ 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_{\infty }\text{,}$ since $\mathbb{Z}/0\mathbb{Z}$ is $\mathbb{Z}\text{.}$

D₀≡D∞ : D  ≡ D∞
D₀≡D∞ = ap Dih ℤ-ab/0≡ℤ-ab