dihedral groups

src/README.lagda.md

@@ -531,6 +531,8 @@ open import group-theory.concrete-group-actions
 open import group-theory.concrete-groups
 open import group-theory.conjugation
 open import group-theory.contravariant-pushforward-concrete-group-actions
+open import group-theory.dihedral-group-construction
+open import group-theory.dihedral-groups
 open import group-theory.e8-lattice
 open import group-theory.embeddings-groups
 open import group-theory.endomorphism-rings-abelian-groups

src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md

@@ -10,12 +10,14 @@ module elementary-number-theory.groups-of-modular-arithmetic where
 open import elementary-number-theory.modular-arithmetic using
   ( ℤ-Mod-Set; add-ℤ-Mod; associative-add-ℤ-Mod; zero-ℤ-Mod; neg-ℤ-Mod;
     left-unit-law-add-ℤ-Mod; right-unit-law-add-ℤ-Mod;
-    left-inverse-law-add-ℤ-Mod; right-inverse-law-add-ℤ-Mod)
+    left-inverse-law-add-ℤ-Mod; right-inverse-law-add-ℤ-Mod;
+    commutative-add-ℤ-Mod)
 open import elementary-number-theory.natural-numbers using (ℕ)
 
 open import foundation.dependent-pair-types using (Σ; pair; pr1; pr2)
 open import foundation.universe-levels using (lzero)
 
+open import group-theory.abelian-groups using (Ab)
 open import group-theory.groups using (Group)
 open import group-theory.semigroups using (Semigroup)
 ```
@@ -40,4 +42,8 @@ pr2 (pr2 (pr1 (pr2 (ℤ-Mod-Group k)))) = right-unit-law-add-ℤ-Mod k
 pr1 (pr2 (pr2 (ℤ-Mod-Group k))) = neg-ℤ-Mod k
 pr1 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = left-inverse-law-add-ℤ-Mod k
 pr2 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = right-inverse-law-add-ℤ-Mod k
+
+ℤ-Mod-Ab : (k : ℕ) → Ab lzero
+pr1 (ℤ-Mod-Ab k) = ℤ-Mod-Group k
+pr2 (ℤ-Mod-Ab k) = commutative-add-ℤ-Mod k
 ```

src/group-theory.lagda.md

@@ -23,6 +23,8 @@ open import group-theory.concrete-group-actions public
 open import group-theory.concrete-groups public
 open import group-theory.conjugation public
 open import group-theory.contravariant-pushforward-concrete-group-actions public
+open import group-theory.dihedral-group-construction public
+open import group-theory.dihedral-groups public
 open import group-theory.e8-lattice public
 open import group-theory.embeddings-groups public
 open import group-theory.endomorphism-rings-abelian-groups public

src/group-theory/abelian-groups.lagda.md

@@ -12,7 +12,7 @@ open import foundation.binary-equivalences using (is-binary-equiv)
 open import foundation.dependent-pair-types using (Σ; pair; pr1; pr2)
 open import foundation.embeddings using (is-emb)
 open import foundation.equivalences using (is-equiv)
-open import foundation.identity-types using (Id; ap-binary; _∙_; inv)
+open import foundation.identity-types using (Id; _＝_; ap-binary; _∙_; inv)
 open import foundation.injective-maps using (is-injective)
 open import foundation.interchange-law using
   (interchange-law-commutative-and-associative)
@@ -32,7 +32,7 @@ open import group-theory.groups using
     transpose-eq-mul-Group'; is-binary-emb-mul-Group; is-emb-mul-Group;
     is-emb-mul-Group'; is-injective-mul-Group; is-injective-mul-Group';
     is-idempotent-Group; is-unit-is-idempotent-Group; mul-list-Group;
-    preserves-concat-mul-list-Group)
+    preserves-concat-mul-list-Group; inv-inv-Group; inv-unit-Group)
 open import group-theory.monoids using (is-unital-Semigroup)
 open import group-theory.semigroups using
   ( has-associative-mul-Set; Semigroup)
@@ -172,6 +172,13 @@ distributive-neg-add-Ab :
 distributive-neg-add-Ab A x y =
   ( distributive-inv-mul-Group (group-Ab A) x y) ∙
   ( commutative-add-Ab A (neg-Ab A y) (neg-Ab A x))
+
+neg-neg-Ab :
+  {l : Level} (A : Ab l) (x : type-Ab A) → neg-Ab A (neg-Ab A x) ＝ x
+neg-neg-Ab A = inv-inv-Group (group-Ab A)
+
+neg-zero-Ab : {l : Level} (A : Ab l) → neg-Ab A (zero-Ab A) ＝ zero-Ab A
+neg-zero-Ab A = inv-unit-Group (group-Ab A)
 ```
 
 ### Addition on an abelian group is a binary equivalence

src/group-theory/dihedral-group-construction.lagda.md

@@ -0,0 +1,150 @@
+---
+title: The dihedral group construction
+---
+
+```agda
+module group-theory.dihedral-group-construction where
+
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equality-coproduct-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.groups
+open import group-theory.monoids
+open import group-theory.semigroups
+```
+
+## Idea
+
+When `A` is an abelian group, we can put a group structure on the disjoint union `A+A`, which specializes to the dihedral groups when we take `A := ℤ/k`.
+
+## Definitions
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  set-dihedral-group-Ab : UU-Set l
+  set-dihedral-group-Ab = coprod-Set (set-Ab A) (set-Ab A)
+
+  type-dihedral-group-Ab : UU l
+  type-dihedral-group-Ab = type-Set set-dihedral-group-Ab
+
+  is-set-type-dihedral-group-Ab : is-set type-dihedral-group-Ab
+  is-set-type-dihedral-group-Ab = is-set-type-Set set-dihedral-group-Ab
+
+  unit-dihedral-group-Ab : type-dihedral-group-Ab
+  unit-dihedral-group-Ab = inl (zero-Ab A)
+
+  mul-dihedral-group-Ab :
+    (x y : type-dihedral-group-Ab) → type-dihedral-group-Ab
+  mul-dihedral-group-Ab (inl x) (inl y) = inl (add-Ab A x y)
+  mul-dihedral-group-Ab (inl x) (inr y) = inr (add-Ab A (neg-Ab A x) y)
+  mul-dihedral-group-Ab (inr x) (inl y) = inr (add-Ab A x y)
+  mul-dihedral-group-Ab (inr x) (inr y) = inl (add-Ab A (neg-Ab A x) y)
+
+  inv-dihedral-group-Ab : type-dihedral-group-Ab → type-dihedral-group-Ab
+  inv-dihedral-group-Ab (inl x) = inl (neg-Ab A x)
+  inv-dihedral-group-Ab (inr x) = inr x
+
+  associative-mul-dihedral-group-Ab :
+    (x y z : type-dihedral-group-Ab) →
+    (mul-dihedral-group-Ab (mul-dihedral-group-Ab x y) z) ＝
+    (mul-dihedral-group-Ab x (mul-dihedral-group-Ab y z))
+  associative-mul-dihedral-group-Ab (inl x) (inl y) (inl z) =
+    ap inl (associative-add-Ab A x y z)
+  associative-mul-dihedral-group-Ab (inl x) (inl y) (inr z) =
+    ap
+      ( inr)
+      ( ( ap (add-Ab' A z) (distributive-neg-add-Ab A x y)) ∙
+        ( associative-add-Ab A (neg-Ab A x) (neg-Ab A y) z))
+  associative-mul-dihedral-group-Ab (inl x) (inr y) (inl z) =
+    ap inr (associative-add-Ab A (neg-Ab A x) y z)
+  associative-mul-dihedral-group-Ab (inl x) (inr y) (inr z) =
+    ap
+      ( inl)
+      ( ( ap
+          ( add-Ab' A z)
+          ( ( distributive-neg-add-Ab A (neg-Ab A x) y) ∙
+            ( ap (add-Ab' A (neg-Ab A y)) (neg-neg-Ab A x)))) ∙
+        ( associative-add-Ab A x (neg-Ab A y) z))
+  associative-mul-dihedral-group-Ab (inr x) (inl y) (inl z) =
+    ap inr (associative-add-Ab A x y z)
+  associative-mul-dihedral-group-Ab (inr x) (inl y) (inr z) =
+    ap
+      ( inl)
+      ( ( ap (add-Ab' A z) (distributive-neg-add-Ab A x y)) ∙
+        ( associative-add-Ab A (neg-Ab A x) (neg-Ab A y) z))
+  associative-mul-dihedral-group-Ab (inr x) (inr y) (inl z) =
+    ap inl (associative-add-Ab A (neg-Ab A x) y z)
+  associative-mul-dihedral-group-Ab (inr x) (inr y) (inr z) =
+    ap
+      ( inr)
+      ( ( ap
+          ( add-Ab' A z)
+          ( ( distributive-neg-add-Ab A (neg-Ab A x) y) ∙
+            ( ap (add-Ab' A (neg-Ab A y)) (neg-neg-Ab A x)))) ∙
+        ( associative-add-Ab A x (neg-Ab A y) z))
+
+  left-unit-law-mul-dihedral-group-Ab :
+    (x : type-dihedral-group-Ab) →
+    (mul-dihedral-group-Ab unit-dihedral-group-Ab x) ＝ x
+  left-unit-law-mul-dihedral-group-Ab (inl x) =
+    ap inl (left-unit-law-add-Ab A x)
+  left-unit-law-mul-dihedral-group-Ab (inr x) =
+    ap inr (ap (add-Ab' A x) (neg-zero-Ab A) ∙ left-unit-law-add-Ab A x)
+
+  right-unit-law-mul-dihedral-group-Ab :
+    (x : type-dihedral-group-Ab) →
+    (mul-dihedral-group-Ab x unit-dihedral-group-Ab) ＝ x
+  right-unit-law-mul-dihedral-group-Ab (inl x) =
+    ap inl (right-unit-law-add-Ab A x)
+  right-unit-law-mul-dihedral-group-Ab (inr x) =
+    ap inr (right-unit-law-add-Ab A x)
+
+  left-inverse-law-mul-dihedral-group-Ab :
+    (x : type-dihedral-group-Ab) →
+    ( mul-dihedral-group-Ab (inv-dihedral-group-Ab x) x) ＝
+    ( unit-dihedral-group-Ab)
+  left-inverse-law-mul-dihedral-group-Ab (inl x) =
+    ap inl (left-inverse-law-add-Ab A x)
+  left-inverse-law-mul-dihedral-group-Ab (inr x) =
+    ap inl (left-inverse-law-add-Ab A x)
+
+  right-inverse-law-mul-dihedral-group-Ab :
+    (x : type-dihedral-group-Ab) →
+    ( mul-dihedral-group-Ab x (inv-dihedral-group-Ab x)) ＝
+    ( unit-dihedral-group-Ab)
+  right-inverse-law-mul-dihedral-group-Ab (inl x) =
+    ap inl (right-inverse-law-add-Ab A x)
+  right-inverse-law-mul-dihedral-group-Ab (inr x) =
+    ap inl (left-inverse-law-add-Ab A x)
+
+  semigroup-dihedral-group-Ab : Semigroup l
+  pr1 semigroup-dihedral-group-Ab = set-dihedral-group-Ab
+  pr1 (pr2 semigroup-dihedral-group-Ab) = mul-dihedral-group-Ab
+  pr2 (pr2 semigroup-dihedral-group-Ab) = associative-mul-dihedral-group-Ab
+
+  monoid-dihedral-group-Ab : Monoid l
+  pr1 monoid-dihedral-group-Ab = semigroup-dihedral-group-Ab
+  pr1 (pr2 monoid-dihedral-group-Ab) = unit-dihedral-group-Ab
+  pr1 (pr2 (pr2 monoid-dihedral-group-Ab)) = left-unit-law-mul-dihedral-group-Ab
+  pr2 (pr2 (pr2 monoid-dihedral-group-Ab)) =
+    right-unit-law-mul-dihedral-group-Ab
+
+  dihedral-group-Ab : Group l
+  pr1 dihedral-group-Ab = semigroup-dihedral-group-Ab
+  pr1 (pr1 (pr2 dihedral-group-Ab)) = unit-dihedral-group-Ab
+  pr1 (pr2 (pr1 (pr2 dihedral-group-Ab))) = left-unit-law-mul-dihedral-group-Ab
+  pr2 (pr2 (pr1 (pr2 dihedral-group-Ab))) = right-unit-law-mul-dihedral-group-Ab
+  pr1 (pr2 (pr2 dihedral-group-Ab)) = inv-dihedral-group-Ab
+  pr1 (pr2 (pr2 (pr2 dihedral-group-Ab))) =
+    left-inverse-law-mul-dihedral-group-Ab
+  pr2 (pr2 (pr2 (pr2 dihedral-group-Ab))) =
+    right-inverse-law-mul-dihedral-group-Ab
+```

src/group-theory/dihedral-groups.lagda.md

@@ -0,0 +1,26 @@
+---
+title: The dihedral groups
+---
+
+```agda
+module group-theory.dihedral-groups where
+
+open import elementary-number-theory.groups-of-modular-arithmetic
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import group-theory.dihedral-group-construction
+open import group-theory.groups
+```
+
+## Idea
+
+The dihedral group `D_k` is defined by the dihedral group construction applied to the cyclic group `ℤ-Mod k`.
+
+## Definition
+
+```agda
+dihedral-group : ℕ → Group lzero
+dihedral-group k = dihedral-group-Ab (ℤ-Mod-Ab k)
+```

src/group-theory/groups.lagda.md

@@ -155,9 +155,9 @@ module _
     (x : type-Group) → Id (mul-Group x (inv-Group x)) unit-Group
   right-inverse-law-Group = pr2 (pr2 has-inverses-Group)
 
-  is-own-inverse-unit-Group :
+  inv-unit-Group :
     Id (inv-Group unit-Group) unit-Group
-  is-own-inverse-unit-Group =
+  inv-unit-Group =
     ( inv (left-unit-law-Group (inv-Group unit-Group))) ∙
       ( right-inverse-law-Group unit-Group)
 

src/group-theory/kernels.lagda.md

@@ -56,7 +56,7 @@ module _
     is-closed-under-inv-subset-Group G subtype-kernel-hom-Group
   is-closed-under-inv-subtype-kernel-hom-Group x p =
     ( preserves-inv-hom-Group G H f x) ∙
-    ( ap (inv-Group H) p ∙ is-own-inverse-unit-Group H)
+    ( ap (inv-Group H) p ∙ inv-unit-Group H)
 
   subgroup-kernel-hom-Group : Subgroup k G
   pr1 subgroup-kernel-hom-Group = subtype-kernel-hom-Group

src/group-theory/subgroups-generated-by-subsets-groups.lagda.md

@@ -24,7 +24,7 @@ open import foundation.universe-levels using (Level; UU; _⊔_; lsuc)
 
 open import group-theory.groups using
   ( Group; type-Group; unit-Group; mul-Group; inv-Group; left-unit-law-Group;
-    right-unit-law-Group; associative-mul-Group; ap-mul-Group; is-own-inverse-unit-Group;
+    right-unit-law-Group; associative-mul-Group; ap-mul-Group; inv-unit-Group;
     inv-inv-Group; distributive-inv-mul-Group)
 open import group-theory.subgroups using
   ( subset-Group; Subgroup; subset-Subgroup; is-in-Subgroup; contains-unit-Subgroup;
@@ -117,7 +117,7 @@ module _
          ( inv-formal-combination-subset-Group u))
        ( inv-Group G (ev-formal-combination-subset-Group u))
   preserves-inv-ev-formal-combination-subset-Group nil =
-    inv (is-own-inverse-unit-Group G)
+    inv (inv-unit-Group G)
   preserves-inv-ev-formal-combination-subset-Group (cons (pair (inl (inr star)) x) u) =
     ( preserves-concat-ev-formal-combination-subset-Group
       ( inv-formal-combination-subset-Group u)

src/group-theory/subgroups.lagda.md

@@ -33,7 +33,7 @@ open import group-theory.groups using
   ( Group; type-Group; unit-Group; mul-Group; inv-Group; is-set-type-Group;
     associative-mul-Group; left-unit-law-Group; right-unit-law-Group;
     left-inverse-law-Group; right-inverse-law-Group; is-unit-group-Prop;
-    is-own-inverse-unit-Group; semigroup-Group)
+    inv-unit-Group; semigroup-Group)
 open import group-theory.homomorphisms-groups using
   ( preserves-mul-Group; type-hom-Group; preserves-unit-Group;
     preserves-inverses-Group)
@@ -368,7 +368,7 @@ module _
   pr1 (pr2 (pr2 trivial-Subgroup)) .(unit-Group G) .(unit-Group G) refl refl =
     left-unit-law-Group G (unit-Group G)
   pr2 (pr2 (pr2 trivial-Subgroup)) .(unit-Group G) refl =
-    is-own-inverse-unit-Group G
+    inv-unit-Group G
 ```