initial commit

.gitignore

@@ -0,0 +1 @@
+_build/

GroupTheory.agda-lib

@@ -0,0 +1,3 @@
+name: GroupTheory
+depend: standard-library-2.1
+include: src/

README.org

@@ -0,0 +1,7 @@
+#+title: GroupTheory
+
+Like [[https://forgejo.ballcloud.cc/Category-Theory][my category theory]] formalization, this is a formalization of basic group theory in Agda for learning purposes. My primary goal with this project was to get a better understanding of Agda by formalizing a topic I am very familiar with, rather one that I am actively learning. In particular, I wanted more practice working with different notions of equality, as this is something that comes up in formalizing category theory (you want to abstract over an arbitrary equivalence relation on hom-sets, rather than working with propositional equality, which can be very limiting, e.g. when working with functions as morphisms). As such, my goal, which I accomplished, was to formalize and prove the first isomorphism theorem, as that requires working with multiple groups, subgroups, and quotient groups, all of which require careful understanding of the equivalence relations involved and comfort in working with them.
+
+I have since learned more about how instance arguments work, which would have simplified the notation when working with multiple groups, though the current level of clarity isn't necessarily bad. I may come back and clean that up, as I learned a ton from this project, but regardless of the cleanliness of this library, it is a success in my books.
+
+Unlike my category theory formalization, this was done off the top of my head, rather than being inspired by a particular book, as I am already very familiar with basic algebra. Despite that, Agda's extreme rigor makes sure I haven't made any mathematical mistakes, at least.

src/Group/Core.agda

@@ -0,0 +1,65 @@
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary using (IsEquivalence; Setoid; Rel)
+open import Data.Product using (Σ-syntax)
+
+module Group.Core where
+
+record Group {ℓ₁ ℓ₂ : Level} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
+  infix 5 _≈_
+  infixl 9 _·_
+  infix 10 _⁻¹
+  field
+    G : Set ℓ₁
+    _·_ : G → G → G
+    _⁻¹ : G → G
+    _≈_ : Rel G ℓ₂
+    e : G
+
+    isEquivalence : IsEquivalence _≈_
+    ≈-resp-·ˡ : ∀ {a b c} → a ≈ b → a · c ≈ b · c
+    ≈-resp-·ʳ : ∀ {a b c} → a ≈ b → c · a ≈ c · b
+    ≈-resp-⁻¹ : ∀ {a b} → a ≈ b → a ⁻¹ ≈ b ⁻¹
+    identity-ˡ : ∀ {a} → e · a ≈ a
+    identity-ʳ : ∀ {a} → a · e ≈ a
+    assoc : ∀ {a b c} → a · (b · c) ≈ (a · b) · c
+    inverse-ˡ : ∀ {a} → a ⁻¹ · a ≈ e
+    inverse-ʳ : ∀ {a} → a · a ⁻¹ ≈ e
+
+  setoid : Setoid _ _
+  setoid = record { Carrier = G ; _≈_ = _≈_ ; isEquivalence = isEquivalence }
+
+  module Reasoning where
+    open import Relation.Binary.Reasoning.Setoid setoid public
+    open IsEquivalence isEquivalence public
+
+record Homomorphism {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+                    (𝐆 : Group {ℓ₁} {ℓ₂})
+                    (𝐇 : Group {ℓ₃} {ℓ₄}) : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+  open Group 𝐆 renaming (_≈_ to _≈₁_) using (G; _·_)
+  open Group 𝐇 renaming (_·_ to _∙_; G to H; _≈_ to _≈₂_)
+  field
+    φ : G → H
+    homo : ∀ {a b} → φ (a · b) ≈₂ φ a ∙ φ b
+    φ-resp-≈ : ∀ {a b} → a ≈₁ b → φ a ≈₂ φ b
+
+record Isomorphism {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+                    (𝐆 : Group {ℓ₁} {ℓ₂})
+                    (𝐇 : Group {ℓ₃} {ℓ₄}) : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+  open Group 𝐆 renaming (_≈_ to _≈₁_) using (G)
+  open Group 𝐇 renaming (_≈_ to _≈₂_; G to H)
+  open Homomorphism
+  field
+    F : Homomorphism 𝐆 𝐇
+    inj : ∀ {a b : G} → φ F a ≈₂ φ F b → a ≈₁ b
+    surj : ∀ {h : H} → Σ[ g ∈ G ] φ F g ≈₂ h
+
+record Subgroup {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+                    (𝐇 : Group {ℓ₁} {ℓ₂})
+                    (𝐆 : Group {ℓ₃} {ℓ₄}) : Set (suc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)) where
+
+  open Group 𝐆 renaming (_≈_ to _≈₁_)
+  open Group 𝐇 renaming (_≈_ to _≈₂_)
+  open Homomorphism
+  field
+    F : Homomorphism 𝐇 𝐆
+    inj : ∀ {a b : G 𝐇} → φ F a ≈₁ φ F b → a ≈₂ b

src/Group/FirstIsomorphism.agda

@@ -0,0 +1,80 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (Σ-syntax; _×_; _,_; proj₁; proj₂)
+import Group.HomomorphismProperties
+import Group.Kernel
+import Group.Image
+open import Group.QuotientGroup
+
+import Group.Properties
+open import Group.SubgroupTests
+
+module Group.FirstIsomorphism
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (𝐇 : Group {ℓ₃} {ℓ₄})
+       (F : Homomorphism 𝐆 𝐇)
+       where
+
+private
+  module GM = Group 𝐆
+  module HM = Group 𝐇
+  module GP = Group.Properties 𝐆
+  module HP = Group.Properties 𝐇
+  open Group 𝐆 renaming (e to eᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈₁_) using (_·_; G)
+  open Group 𝐇 renaming (e to eᴴ; _⁻¹ to _⁻¹ᴴ; _·_ to _∙_; G to H; _≈_ to _≈₂_) using ()
+
+  module F = Homomorphism F
+
+  open Group.HomomorphismProperties 𝐆 𝐇 F
+  open Group.Kernel 𝐆 𝐇 F
+  open Group.Image 𝐆 𝐇 F
+
+G/kerφ : Group
+G/kerφ = quotient kernel-group 𝐆 kernel-subgroup kernel-normal
+
+imφ : Group
+imφ = image-group
+
+private
+  module G/k = Group G/kerφ
+  module im = Group imφ
+
+nat-hom : Homomorphism G/kerφ imφ
+nat-hom = record
+  { φ = λ g → (φ g) , (g , refl)
+  ; homo = homo
+  ; φ-resp-≈ = λ {a} {b} ((g , φg≈e) , φg≈ab⁻¹) →
+    begin
+      φ a                                     ≈⟨ sym HM.identity-ˡ ⟩
+      eᴴ ∙ φ a                                ≈⟨ HM.≈-resp-·ˡ (trans (sym HM.inverse-ˡ) HM.identity-ʳ) ⟩
+      eᴴ ⁻¹ᴴ ∙ φ a                            ≈⟨ HM.≈-resp-·ˡ (HM.≈-resp-⁻¹ (trans (sym φg≈e) (φ-resp-≈ φg≈ab⁻¹))) ⟩
+      (φ (a · b ⁻¹ᴳ)) ⁻¹ᴴ ∙ φ a               ≈⟨ HM.≈-resp-·ˡ (sym preserve-⁻¹) ⟩
+      φ ((a · b ⁻¹ᴳ) ⁻¹ᴳ) ∙ φ a               ≈⟨ HM.≈-resp-·ˡ (φ-resp-≈ (GM.Reasoning.sym GP.shoes-and-socks)) ⟩
+      φ (b ⁻¹ᴳ ⁻¹ᴳ · a ⁻¹ᴳ) ∙ φ a             ≈⟨ HM.≈-resp-·ˡ (φ-resp-≈ (GM.≈-resp-·ˡ (GM.Reasoning.sym GP.⁻¹-involutive))) ⟩
+      φ (b · a ⁻¹ᴳ) ∙ φ a                     ≈⟨ sym homo ⟩
+      φ (b · a ⁻¹ᴳ · a)                       ≈⟨ sym (φ-resp-≈ GM.assoc) ⟩
+      φ (b · (a ⁻¹ᴳ · a))                     ≈⟨ φ-resp-≈ (GM.≈-resp-·ʳ GM.inverse-ˡ) ⟩
+      φ (b · eᴳ)                              ≈⟨ φ-resp-≈ GM.identity-ʳ ⟩
+      φ b
+    ∎
+  }
+  where open HM.Reasoning
+        open F
+
+nat-hom-iso : Isomorphism G/kerφ imφ
+nat-hom-iso = record
+  { F = nat-hom
+  ; inj = λ {a} {b} φa≈φb → (a · b ⁻¹ᴳ , (
+    begin
+      φ (a · b ⁻¹ᴳ)     ≈⟨ homo ⟩
+      φ a ∙ φ (b ⁻¹ᴳ)   ≈⟨ HM.≈-resp-·ʳ preserve-⁻¹ ⟩
+      φ a ∙ (φ b) ⁻¹ᴴ   ≈⟨ HM.≈-resp-·ʳ (HM.≈-resp-⁻¹ (sym φa≈φb)) ⟩
+      φ a ∙ (φ a) ⁻¹ᴴ   ≈⟨ HM.inverse-ʳ ⟩
+      eᴴ
+    ∎
+  )) , GM.Reasoning.refl
+  ; surj = λ {(_ , h′ , φh′≈h)} → h′ , φh′≈h
+  }
+  where open HM.Reasoning
+        open F

src/Group/Homomorphism.agda

@@ -0,0 +1,18 @@
+open import Level using (Level; _⊔_)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; cong; sym; trans)
+open Eq.≡-Reasoning
+open import Group.Definition
+
+module Group.Homomorphism where
+
+record Homomorphism {ℓ₁ ℓ₂ : Level} (𝐆 : Group {ℓ₁}) (𝐇 : Group {ℓ₂}) : Set (ℓ₁ ⊔ ℓ₂) where
+  open Group 𝐆 renaming (_·_ to _*_) using (G)
+  open Group 𝐇 renaming (_·_ to _∙_; G to H) using (e)
+  field
+    φ : G → H
+    homo : ∀ {a b} → φ (a * b) ≡ φ a ∙ φ b
+
+  module Defs where
+    ker : G → Set _
+    ker g = φ g ≡ e

src/Group/HomomorphismProperties.agda

@@ -0,0 +1,38 @@
+open import Group.Core
+open import Level using (Level)
+
+import Group.Properties
+
+module Group.HomomorphismProperties
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (𝐇 : Group {ℓ₃} {ℓ₄})
+       (F : Homomorphism 𝐆 𝐇)
+       where
+
+private
+  module GM = Group 𝐆
+  module HM = Group 𝐇
+  open Group 𝐆 renaming (e to eᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈₁_) using (_·_; G)
+  open Group 𝐇 renaming (e to eᴴ; _⁻¹ to _⁻¹ᴴ; _·_ to _∙_; G to H; _≈_ to _≈₂_) using ()
+
+  open Homomorphism F
+
+  module GP = Group.Properties 𝐆
+  module HP = Group.Properties 𝐇
+
+preserve-e : φ eᴳ ≈₂ eᴴ
+preserve-e = HP.cancel-ˡ (begin
+    φ eᴳ ∙ φ eᴳ ≈⟨ sym homo ⟩
+    φ (eᴳ · eᴳ) ≈⟨ φ-resp-≈ GM.identity-ˡ ⟩
+    φ eᴳ        ≈⟨ sym HM.identity-ʳ ⟩
+    φ eᴳ ∙ eᴴ ∎)
+    where open HM.Reasoning
+
+preserve-⁻¹ : ∀ {a} → φ (a ⁻¹ᴳ) ≈₂ (φ a) ⁻¹ᴴ
+preserve-⁻¹ {a} = HP.uniq-inverse-ˡ (begin
+    φ (a ⁻¹ᴳ) ∙ φ a ≈⟨ sym homo ⟩
+    φ (a ⁻¹ᴳ · a)   ≈⟨ φ-resp-≈ GM.inverse-ˡ ⟩
+    φ eᴳ            ≈⟨ preserve-e ⟩
+    eᴴ ∎)
+    where open HM.Reasoning

src/Group/Image.agda

@@ -0,0 +1,51 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (Σ-syntax; _×_; _,_; proj₁; proj₂)
+import Group.HomomorphismProperties
+open import Group.NormalSubgroup
+
+import Group.Properties
+open import Group.SubgroupTests
+
+module Group.Image
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (𝐇 : Group {ℓ₃} {ℓ₄})
+       (F : Homomorphism 𝐆 𝐇)
+       where
+
+private
+  module GM = Group 𝐆
+  module HM = Group 𝐇
+  open Group 𝐆 renaming (e to eᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈₁_) using (_·_; G)
+  open Group 𝐇 renaming (e to eᴴ; _⁻¹ to _⁻¹ᴴ; _·_ to _∙_; G to H; _≈_ to _≈₂_) using ()
+
+  open Homomorphism F
+
+  module GP = Group.Properties 𝐆
+  module HP = Group.Properties 𝐇
+
+  open Group.HomomorphismProperties 𝐆 𝐇 F
+
+image : Set _
+image = Σ[ h ∈ H ] Σ[ g ∈ G ] φ g ≈₂ h
+
+ι : image → H
+ι = proj₁
+
+image-closed-· : ∀ (a b : image) → Σ[ c ∈ image ] ι c ≈₂ ι a ∙ ι b
+image-closed-· (a , a′ , ha) (b , b′ , hb) = ((a ∙ b) , ((a′ · b′) , trans homo (trans (HM.≈-resp-·ˡ ha) (HM.≈-resp-·ʳ hb)))) , refl
+  where open HM.Reasoning
+
+image-closed-⁻¹ : ∀ (a : image) → Σ[ a⁻¹ ∈ image ] ι a⁻¹ ≈₂ (ι a) ⁻¹ᴴ
+image-closed-⁻¹ (a , a′ , ha) = ((a ⁻¹ᴴ) , ((a′ ⁻¹ᴳ) , trans preserve-⁻¹ (HM.≈-resp-⁻¹ ha))) , refl
+  where open HM.Reasoning
+
+image-closed-e : Σ[ e′ ∈ image ] ι e′ ≈₂ eᴴ
+image-closed-e = (eᴴ , (eᴳ , preserve-e)) , HM.Reasoning.refl
+
+image-group : Group
+image-group = two-step 𝐇 image ι image-closed-· image-closed-⁻¹ image-closed-e
+
+image-subgroup : Subgroup image-group 𝐇
+image-subgroup = two-step-subgroup 𝐇 image ι image-closed-· image-closed-⁻¹ image-closed-e

src/Group/Kernel.agda

@@ -0,0 +1,63 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (Σ-syntax; _×_; _,_; proj₁; proj₂)
+import Group.HomomorphismProperties
+open import Group.NormalSubgroup
+
+import Group.Properties
+open import Group.SubgroupTests
+
+module Group.Kernel
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (𝐇 : Group {ℓ₃} {ℓ₄})
+       (F : Homomorphism 𝐆 𝐇)
+       where
+
+private
+  module GM = Group 𝐆
+  module HM = Group 𝐇
+  open Group 𝐆 renaming (e to eᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈₁_) using (_·_; G)
+  open Group 𝐇 renaming (e to eᴴ; _⁻¹ to _⁻¹ᴴ; _·_ to _∙_; G to H; _≈_ to _≈₂_) using ()
+
+  open Homomorphism F
+
+  module GP = Group.Properties 𝐆
+  module HP = Group.Properties 𝐇
+
+  open Group.HomomorphismProperties 𝐆 𝐇 F
+
+kernel : Set _
+kernel = Σ[ g ∈ G ] φ g ≈₂ eᴴ
+
+ι : kernel → G
+ι = proj₁
+
+kernel-closed-· : ∀ (a b : kernel) → Σ[ c ∈ kernel ] ι c ≈₁ ι a · ι b
+kernel-closed-· (a , ha) (b , hb) = (a · b , trans homo (trans (trans (HM.≈-resp-·ˡ ha) HM.identity-ˡ) hb)) , GM.Reasoning.refl
+                where open HM.Reasoning
+
+kernel-closed-⁻¹ : ∀ (a : kernel) → Σ[ a⁻¹ ∈ kernel ] ι a⁻¹ ≈₁ (ι a) ⁻¹ᴳ
+kernel-closed-⁻¹ (a , ha) = (a ⁻¹ᴳ , trans (trans preserve-⁻¹ (HM.≈-resp-⁻¹ ha)) (sym HP.e≈e⁻¹)) , GM.Reasoning.refl
+                 where open HM.Reasoning
+
+kernel-closed-e : Σ[ e′ ∈ kernel ] ι e′ ≈₁ eᴳ
+kernel-closed-e = (eᴳ , preserve-e) , GM.Reasoning.refl
+
+kernel-group : Group
+kernel-group = two-step 𝐆 kernel ι kernel-closed-· kernel-closed-⁻¹ kernel-closed-e
+
+kernel-subgroup : Subgroup kernel-group 𝐆
+kernel-subgroup = two-step-subgroup 𝐆 kernel ι kernel-closed-· kernel-closed-⁻¹ kernel-closed-e
+
+kernel-normal : normal kernel-group 𝐆 kernel-subgroup
+kernel-normal (h , hh) g = (g · h · g ⁻¹ᴳ , (begin
+    φ (g · h · g ⁻¹ᴳ)      ≈⟨ homo ⟩
+    φ (g · h) ∙ φ (g ⁻¹ᴳ)  ≈⟨ HM.≈-resp-·ˡ homo ⟩
+    φ g ∙ φ h ∙ φ (g ⁻¹ᴳ)  ≈⟨ HM.≈-resp-·ˡ (HM.≈-resp-·ʳ hh) ⟩
+    φ g ∙ eᴴ ∙ φ (g ⁻¹ᴳ)   ≈⟨ HM.≈-resp-·ˡ HM.identity-ʳ ⟩
+    φ g ∙ φ (g ⁻¹ᴳ)        ≈⟨ HM.≈-resp-·ʳ preserve-⁻¹ ⟩
+    φ g ∙ (φ g) ⁻¹ᴴ        ≈⟨ HM.inverse-ʳ ⟩
+    eᴴ ∎)) ,
+  GM.≈-resp-·ˡ GM.Reasoning.refl
+  where open HM.Reasoning

src/Group/NormalSubgroup.agda

@@ -0,0 +1,19 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (Σ-syntax)
+
+module Group.NormalSubgroup
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐇 : Group {ℓ₁} {ℓ₂})
+       (𝐆 : Group {ℓ₃} {ℓ₄})
+       (𝐇≤𝐆 : Subgroup 𝐇 𝐆)
+       where
+
+open Group 𝐆 using (G; _·_; _≈_; _⁻¹)
+open Group 𝐇 renaming (G to H) using ()
+open Subgroup 𝐇≤𝐆
+open Homomorphism F
+
+normal : Set _
+normal = ∀ (h : H) → ∀ (g : G) →
+    Σ[ h′ ∈ H ] φ h′ ≈ g · φ h · g ⁻¹

src/Group/Properties.agda

@@ -0,0 +1,72 @@
+open import Group.Core
+open import Data.Product using (_×_)
+
+module Group.Properties {ℓ₁ ℓ₂} (𝐆 : Group {ℓ₁} {ℓ₂}) where
+
+open Group 𝐆
+open Reasoning
+
+private
+  variable
+    a b c : G
+
+uniq-identity : ∀ {a} → (∀ b → b · a ≈ b) → a ≈ e
+uniq-identity {a} h = begin
+    a         ≈⟨ sym identity-ˡ ⟩
+    e · a     ≈⟨ h e ⟩
+    e ∎
+
+cancel-ˡ : ∀ {a b c} → a · b ≈ a · c → b ≈ c
+cancel-ˡ {a} {b} {c} h = begin
+    b               ≈⟨ sym identity-ˡ ⟩
+    e · b           ≈⟨ sym (≈-resp-·ˡ inverse-ˡ) ⟩
+    (a ⁻¹ · a) · b  ≈⟨ sym assoc ⟩
+    a ⁻¹ · (a · b)  ≈⟨ ≈-resp-·ʳ h ⟩
+    a ⁻¹ · (a · c)  ≈⟨ assoc ⟩
+    (a ⁻¹ · a) · c  ≈⟨ ≈-resp-·ˡ inverse-ˡ ⟩
+    e · c           ≈⟨ identity-ˡ ⟩
+    c ∎
+
+cancel-ʳ : ∀ {a b c} → a · b ≈ c · b → a ≈ c
+cancel-ʳ {a} {b} {c} h = begin
+    a               ≈⟨ sym identity-ʳ ⟩
+    a · e           ≈⟨ sym (≈-resp-·ʳ inverse-ʳ) ⟩
+    a · (b · b ⁻¹)  ≈⟨ assoc ⟩
+    (a · b) · b ⁻¹  ≈⟨ ≈-resp-·ˡ h ⟩
+    (c · b) · b ⁻¹  ≈⟨ sym assoc ⟩
+    c · (b · b ⁻¹)  ≈⟨ ≈-resp-·ʳ inverse-ʳ ⟩
+    c · e           ≈⟨ identity-ʳ ⟩
+    c ∎
+
+uniq-inverse-ˡ : ∀ {a b} → a · b ≈ e → a ≈ b ⁻¹
+uniq-inverse-ˡ {a} {b} h = begin
+    a                ≈⟨ sym identity-ʳ ⟩
+    a · e            ≈⟨ sym (≈-resp-·ʳ inverse-ʳ) ⟩
+    a · (b · b ⁻¹)   ≈⟨ assoc ⟩
+    (a · b) · b ⁻¹   ≈⟨ ≈-resp-·ˡ h ⟩
+    e · b ⁻¹         ≈⟨ identity-ˡ ⟩
+    b ⁻¹ ∎
+
+uniq-inverse-ʳ : ∀ {a b} → a · b ≈ e → b ≈ a ⁻¹
+uniq-inverse-ʳ {a} {b} h = begin
+    b                ≈⟨ sym identity-ˡ ⟩
+    e · b            ≈⟨ sym (≈-resp-·ˡ inverse-ˡ) ⟩
+    (a ⁻¹ · a) · b   ≈⟨ sym assoc ⟩
+    a ⁻¹ · (a · b)   ≈⟨ ≈-resp-·ʳ h ⟩
+    a ⁻¹ · e         ≈⟨ identity-ʳ ⟩
+    a ⁻¹ ∎
+
+e≈e⁻¹ : e ≈ e ⁻¹
+e≈e⁻¹ = uniq-inverse-ʳ identity-ˡ
+
+⁻¹-involutive : ∀ {a} → a ≈ a ⁻¹ ⁻¹
+⁻¹-involutive {a} = uniq-inverse-ʳ inverse-ˡ
+
+shoes-and-socks : ∀ {a b} → b ⁻¹ · a ⁻¹ ≈ (a · b) ⁻¹
+shoes-and-socks {a} {b} = uniq-inverse-ʳ (begin
+    (a · b) · (b ⁻¹ · a ⁻¹)              ≈⟨ sym assoc ⟩
+    a · (b · (b ⁻¹ · a ⁻¹))              ≈⟨ ≈-resp-·ʳ assoc ⟩
+    a · (b · b ⁻¹ · a ⁻¹)                ≈⟨ ≈-resp-·ʳ (≈-resp-·ˡ inverse-ʳ) ⟩
+    a · (e · a ⁻¹)                       ≈⟨ ≈-resp-·ʳ identity-ˡ ⟩
+    a · a ⁻¹                             ≈⟨ inverse-ʳ ⟩
+    e ∎)

src/Group/QuotientGroup.agda

@@ -0,0 +1,85 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (Σ-syntax; _,_)
+
+module Group.QuotientGroup
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐍 : Group {ℓ₁} {ℓ₂})
+       (𝐆 : Group {ℓ₃} {ℓ₄})
+       (𝐍≤𝐆 : Subgroup 𝐍 𝐆)
+       where
+
+open import Group.NormalSubgroup
+open Group 𝐆
+open Reasoning
+open Group 𝐍 renaming (G to N; e to e′; _⁻¹ to _⁻¹ᴺ; _·_ to _∙_) using ()
+open Subgroup 𝐍≤𝐆
+open Homomorphism F
+open import Group.HomomorphismProperties 𝐍 𝐆 F using (preserve-e; preserve-⁻¹)
+open import Group.Properties 𝐆
+
+quotient : normal 𝐍 𝐆 𝐍≤𝐆 → Group
+quotient hn =
+  record
+  { G = G
+  ; _·_ = _·_
+  ; _⁻¹ = _⁻¹
+  ; _≈_ = λ g h → Σ[ n ∈ N ] φ n ≈ g · h ⁻¹
+  ; e = e
+  ; isEquivalence = record
+    { refl = e′ , trans preserve-e (sym inverse-ʳ)
+    ; sym = λ {x} {y} (n , φn≈x·y⁻¹) → n ⁻¹ᴺ , (begin
+        φ (n ⁻¹ᴺ)        ≈⟨ preserve-⁻¹ ⟩
+        (φ n) ⁻¹         ≈⟨ ≈-resp-⁻¹ φn≈x·y⁻¹ ⟩
+        (x · y ⁻¹) ⁻¹    ≈⟨ sym shoes-and-socks ⟩
+        y ⁻¹ ⁻¹ · x ⁻¹   ≈⟨ ≈-resp-·ˡ (sym ⁻¹-involutive) ⟩
+        y · x ⁻¹ ∎)
+    ; trans = λ {a} {b} {c} (n₁ , φn₁≈a·b⁻¹) (n₂ , φn₂≈b·c⁻¹) →
+      n₁ ∙ n₂ , (begin
+        φ (n₁ ∙ n₂)                     ≈⟨ homo ⟩
+        φ n₁ · φ n₂                     ≈⟨ ≈-resp-·ˡ φn₁≈a·b⁻¹ ⟩
+        (a · b ⁻¹) · φ n₂               ≈⟨ ≈-resp-·ʳ φn₂≈b·c⁻¹ ⟩
+        (a · b ⁻¹) · (b · c ⁻¹)         ≈⟨ assoc ⟩
+        (a · b ⁻¹ · b) · c ⁻¹           ≈⟨ sym (≈-resp-·ˡ assoc) ⟩
+        (a · (b ⁻¹ · b)) · c ⁻¹         ≈⟨ ≈-resp-·ˡ (≈-resp-·ʳ inverse-ˡ) ⟩
+        (a · e) · c ⁻¹                  ≈⟨ ≈-resp-·ˡ identity-ʳ ⟩
+        a · c ⁻¹ ∎)
+    }
+  ; ≈-resp-·ˡ = λ {a} {b} {c} (n , φn≈a·b⁻¹) → n , (begin
+       φ n                         ≈⟨ φn≈a·b⁻¹ ⟩
+       a · b ⁻¹                    ≈⟨ sym (≈-resp-·ʳ identity-ˡ) ⟩
+       a · (e · b ⁻¹)              ≈⟨ ≈-resp-·ʳ (≈-resp-·ˡ (sym inverse-ʳ)) ⟩
+       a · (c · c ⁻¹ · b ⁻¹)       ≈⟨ sym (≈-resp-·ʳ assoc) ⟩
+       a · (c · (c ⁻¹ · b ⁻¹))     ≈⟨ assoc ⟩
+       a · c · (c ⁻¹ · b ⁻¹)       ≈⟨ ≈-resp-·ʳ shoes-and-socks ⟩
+       a · c · (b · c) ⁻¹ ∎)
+  ; ≈-resp-·ʳ = λ {a} {b} {c} (n , n≈a·b⁻¹) →
+    let (n′ , φn′≈c·φn·c⁻¹) = hn n c in n′ , (begin
+      φ n′ ≈⟨ φn′≈c·φn·c⁻¹ ⟩
+      c · φ n · c ⁻¹ ≈⟨ ≈-resp-·ˡ (≈-resp-·ʳ n≈a·b⁻¹) ⟩
+      c · (a · b ⁻¹) · c ⁻¹ ≈⟨ sym assoc ⟩
+      c · (a · b ⁻¹ · c ⁻¹) ≈⟨ sym (≈-resp-·ʳ assoc) ⟩
+      c · (a · (b ⁻¹ · c ⁻¹)) ≈⟨ assoc ⟩
+      c · a · (b ⁻¹ · c ⁻¹) ≈⟨ ≈-resp-·ʳ shoes-and-socks ⟩
+      c · a · (c · b) ⁻¹ ∎)
+  ; ≈-resp-⁻¹ = λ {a} {b} (n , φn≈a·b⁻¹) →
+    let (n′ , φn′≈a⁻¹·φn·a) = hn n (a ⁻¹) in n′ ⁻¹ᴺ , (begin
+        φ (n′ ⁻¹ᴺ)                        ≈⟨ preserve-⁻¹ ⟩
+        (φ n′) ⁻¹                         ≈⟨ ≈-resp-⁻¹ φn′≈a⁻¹·φn·a ⟩
+        (a ⁻¹ · φ n · (a ⁻¹) ⁻¹) ⁻¹       ≈⟨ ≈-resp-⁻¹ (≈-resp-·ʳ (sym ⁻¹-involutive)) ⟩
+        (a ⁻¹ · φ n · a) ⁻¹               ≈⟨ ≈-resp-⁻¹ (≈-resp-·ˡ (≈-resp-·ʳ φn≈a·b⁻¹)) ⟩
+        (a ⁻¹ · (a · b ⁻¹) · a) ⁻¹        ≈⟨ ≈-resp-⁻¹ (≈-resp-·ˡ assoc) ⟩
+        ((a ⁻¹ · a · b ⁻¹) · a) ⁻¹        ≈⟨ ≈-resp-⁻¹ (≈-resp-·ˡ (≈-resp-·ˡ inverse-ˡ)) ⟩
+        ((e · b ⁻¹) · a) ⁻¹               ≈⟨ ≈-resp-⁻¹ (≈-resp-·ˡ identity-ˡ) ⟩
+        (b ⁻¹ · a) ⁻¹                     ≈⟨ sym shoes-and-socks ⟩
+        a ⁻¹ · (b ⁻¹) ⁻¹ ∎)
+  ; identity-ˡ = e′ , trans preserve-e (trans (sym inverse-ʳ) (≈-resp-·ʳ (≈-resp-⁻¹ identity-ˡ)))
+  ; identity-ʳ = e′ , trans preserve-e (trans (sym inverse-ʳ) (≈-resp-·ʳ (≈-resp-⁻¹ identity-ʳ)))
+  ; assoc = λ {a} {b} {c} → e′ , (begin
+          φ e′ ≈⟨ preserve-e ⟩
+          e ≈⟨ sym inverse-ʳ ⟩
+          (a · b · c) · (a · b · c) ⁻¹ ≈⟨ sym (≈-resp-·ˡ assoc) ⟩
+          a · (b · c) · (a · b · c) ⁻¹ ∎)
+  ; inverse-ˡ = e′ , trans preserve-e (trans (sym inverse-ʳ) (≈-resp-·ˡ (sym inverse-ˡ)))
+  ; inverse-ʳ = e′ , trans preserve-e (trans (sym inverse-ʳ) ((≈-resp-·ˡ (sym inverse-ʳ))))
+  }

src/Group/SubgroupProperties.agda

@@ -0,0 +1,19 @@
+open import Group.Core
+open import Level using (Level)
+
+import Group.Properties
+
+module Group.SubgroupProperties
+       {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (𝐇 : Group {ℓ₃} {ℓ₄})
+       (i : Subgroup 𝐇 𝐆)
+       where
+
+module GM = Group 𝐆
+module HM = Group 𝐇
+open Group 𝐆 renaming (e to eᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈₁_) using (_·_; G)
+open Group 𝐇 renaming (e to eᴴ; _⁻¹ to _⁻¹ᴴ; _·_ to _∙_; G to H; _≈_ to _≈₂_) using ()
+
+open Subgroup i
+open Homomorphism F

src/Group/SubgroupTests.agda

@@ -0,0 +1,107 @@
+open import Group.Core
+open import Level using (Level)
+open import Data.Product using (_,_; Σ-syntax; proj₁; proj₂)
+open import Function using (_$_; _∘_; id)
+
+import Group.Properties
+
+module Group.SubgroupTests
+       {ℓ₁ ℓ₂ ℓ₃ : Level}
+       (𝐆 : Group {ℓ₁} {ℓ₂})
+       (H : Set ℓ₃)
+       where
+
+open Group 𝐆
+
+two-step : (ι : H → G)
+         → (∀ (a b : H) → Σ[ c ∈ H ] ι c ≈ ι a · ι b)
+         → (∀ (a : H) → Σ[ a⁻¹ ∈ H ] ι a⁻¹ ≈ (ι a) ⁻¹)
+         → Σ[ e′ ∈ H ] (ι e′ ≈ e)
+         → Group
+two-step ι ·-closed ⁻¹-closed (e′ , ιe′≈e) =
+  record
+    { G = H
+    ; _·_ = λ g → proj₁ ∘ ·-closed g
+    ; _⁻¹ = proj₁ ∘ ⁻¹-closed
+    ; _≈_ = λ g h → ι g ≈ ι h
+    ; e = e′
+    ; isEquivalence = record
+      { refl = refl
+      ; sym = sym
+      ; trans = trans
+      }
+    ; ≈-resp-·ˡ = λ {a} {b} {c} ιa≈ιb →
+      let (a·c , ιa·c≈ιa·ιc) = ·-closed a c in
+      let (b·c , ιb·c≈ιb·ιc) = ·-closed b c in begin
+        ι a·c                ≈⟨ ιa·c≈ιa·ιc ⟩
+        ι a · ι c            ≈⟨ ≈-resp-·ˡ ιa≈ιb ⟩
+        ι b · ι c            ≈⟨ sym ιb·c≈ιb·ιc ⟩
+        ι b·c ∎
+    ; ≈-resp-·ʳ = λ {a} {b} {c} ιa≈ιb →
+      let (c·a , ιc·a≈ιc·ιa) = ·-closed c a in
+      let (c·b , ιc·b≈ιc·ιb) = ·-closed c b in begin
+        ι c·a                ≈⟨ ιc·a≈ιc·ιa ⟩
+        ι c · ι a            ≈⟨ ≈-resp-·ʳ ιa≈ιb ⟩
+        ι c · ι b            ≈⟨ sym ιc·b≈ιc·ιb ⟩
+        ι c·b ∎
+    ; ≈-resp-⁻¹ = λ {a} {b} ιa≈ιb →
+      let (a⁻¹ , hai) = ⁻¹-closed a in
+      let (b⁻¹ , hbi) = ⁻¹-closed b in begin
+        ι a⁻¹         ≈⟨ hai ⟩
+        (ι a) ⁻¹      ≈⟨ ≈-resp-⁻¹ ιa≈ιb ⟩
+        (ι b) ⁻¹      ≈⟨ sym hbi ⟩
+        ι b⁻¹ ∎
+    ; identity-ˡ = λ {a} →
+      let (e′·a , ιe′·a≈ιe′·ιa) = ·-closed e′ a in begin
+          ι e′·a                ≈⟨ ιe′·a≈ιe′·ιa ⟩
+          ι e′ · ι a            ≈⟨ ≈-resp-·ˡ ιe′≈e ⟩
+          e · ι a               ≈⟨ identity-ˡ ⟩
+          ι a ∎
+    ; identity-ʳ = λ {a} →
+      let (a·e′ , ιa·e′≈ιa·ιe′) = ·-closed a e′ in begin
+          ι a·e′                ≈⟨ ιa·e′≈ιa·ιe′ ⟩
+          ι a · ι e′            ≈⟨ ≈-resp-·ʳ ιe′≈e ⟩
+          ι a · e               ≈⟨ identity-ʳ ⟩
+          ι a ∎
+    ; assoc = λ {a} {b} {c} →
+      let (a·b , hab) = ·-closed a b in
+      let (ab·c , hc) = ·-closed a·b c in
+      let (b·c , hbc) = ·-closed b c in
+      let (a·bc , ha) = ·-closed a b·c in begin
+          ι a·bc                 ≈⟨ ha ⟩
+          ι a · ι b·c            ≈⟨ ≈-resp-·ʳ hbc ⟩
+          ι a · (ι b · ι c)      ≈⟨ assoc ⟩
+          (ι a · ι b) · ι c      ≈⟨ sym (≈-resp-·ˡ hab) ⟩
+          (ι a·b) · ι c          ≈⟨ sym hc ⟩
+          ι ab·c ∎
+    ; inverse-ˡ = λ {a} →
+      let (a⁻¹ , ha⁻¹) = ⁻¹-closed a in
+      let (a⁻¹·a , hboth) = ·-closed a⁻¹ a in begin
+          ι a⁻¹·a         ≈⟨ hboth ⟩
+          ι a⁻¹ · ι a     ≈⟨ ≈-resp-·ˡ ha⁻¹ ⟩
+          (ι a) ⁻¹ · ι a  ≈⟨ inverse-ˡ ⟩
+          e               ≈⟨ sym ιe′≈e ⟩
+          ι e′ ∎
+    ; inverse-ʳ = λ {a} →
+      let (a⁻¹ , ha⁻¹) = ⁻¹-closed a in
+      let (a·a⁻¹ , hboth) = ·-closed a a⁻¹ in begin
+          ι a·a⁻¹         ≈⟨ hboth ⟩
+          ι a · ι a⁻¹     ≈⟨ ≈-resp-·ʳ ha⁻¹ ⟩
+          ι a · (ι a) ⁻¹  ≈⟨ inverse-ʳ ⟩
+          e               ≈⟨ sym ιe′≈e ⟩
+          ι e′ ∎
+    }
+    where open Reasoning
+
+two-step-subgroup : (ι : H → G)
+                  → (h₁ : (∀ (a b : H) → Σ[ c ∈ H ] ι c ≈ ι a · ι b))
+                  → (h₂ : (∀ (a : H) → Σ[ a⁻¹ ∈ H ] ι a⁻¹ ≈ (ι a) ⁻¹))
+                  → (h₃ : Σ[ e′ ∈ H ] (ι e′ ≈ e))
+                  → Subgroup (two-step ι h₁ h₂ h₃) 𝐆
+two-step-subgroup ι h₁ h₂ h₃ = record { F = F ; inj = id }
+                  where
+                    𝐇 = two-step ι h₁ h₂ h₃
+                    F = record
+                      { φ = ι
+                      ; homo = λ {a} {b} → h₁ a b .proj₂
+                      ; φ-resp-≈ = id }