From 14b2cd39dfb2007b4db2c44fa3b462dfe455b889 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 31 Oct 2025 07:34:06 +0100 Subject: [PATCH 01/12] Add normal subgroups and quotient groups --- CHANGELOG.md | 4 + src/Algebra/Construct/Quotient/Group.agda | 127 ++++++++++++++++++++++ src/Algebra/NormalSubgroup.agda | 28 +++++ 3 files changed, 159 insertions(+) create mode 100644 src/Algebra/Construct/Quotient/Group.agda create mode 100644 src/Algebra/NormalSubgroup.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 040b993eae..aab52c2691 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,10 +79,14 @@ Deprecated names New modules ----------- +* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups. + * `Algebra.Construct.Sub.Group` for the definition of subgroups. * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules. +* `Algebra.NormalSubgroup` for the definition of normal subgroups. + * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda new file mode 100644 index 0000000000..ae9fda4644 --- /dev/null +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -0,0 +1,127 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient groups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) +open import Algebra.NormalSubgroup using (NormalSubgroup) + +module Algebra.Construct.Quotient.Group {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where + +open Group G + +import Algebra.Definitions as AlgDefs +open import Algebra.Morphism.Structures using (IsGroupHomomorphism) +open import Algebra.Properties.Monoid monoid +open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) +open import Algebra.Structures using (IsGroup) +open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Function.Definitions using (Surjective) +open import Level using (_⊔_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Binary.Reasoning.Setoid setoid + +private + module N = NormalSubgroup N +open NormalSubgroup N using (ι; module ι; normal) + +infix 0 _by_ + +data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where + _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y + +≋-refl : Reflexive _≋_ +≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x) + +≋-sym : Symmetric _≋_ +≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin + ι (g N.⁻¹) ∙ y ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩ + ι g ⁻¹ ∙ (ι g ∙ x) ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩ + x ∎ + +≋-trans : Transitive _≋_ +≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin + ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩ + (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩ + ι h ∙ y ≈⟨ ιh∙y≈z ⟩ + z ∎ + +≋-isEquivalence : IsEquivalence _≋_ +≋-isEquivalence = record + { refl = ≋-refl + ; sym = ≋-sym + ; trans = ≋-trans + } + +≈⇒≋ : _≈_ ⇒ _≋_ +≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y) + +open AlgDefs _≋_ + +≋-∙-cong : Congruent₂ _∙_ +≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin + ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩ + (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv∙wx≈u[vw∙x] (ι g) (ι h′) x u ⟩ + ι g ∙ ((ι h′ ∙ x) ∙ u) ≈⟨ uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx (normal h x .proj₂) u) (ι g) ⟨ + (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ + y ∙ v ∎ + where h′ = normal h x .proj₁ + +≋-⁻¹-cong : Congruent₁ _⁻¹ +≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin + ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) .proj₂ ⟨ + x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩ + x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨ + (ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩ + y ⁻¹ ∎ + where h = normal (g N.⁻¹) (x ⁻¹) .proj₁ + +quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹ +quotientIsGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≋-isEquivalence + ; ∙-cong = ≋-∙-cong + } + ; assoc = λ x y z → ≈⇒≋ (assoc x y z) + } + ; identity = record + { fst = λ x → ≈⇒≋ (identityˡ x) + ; snd = λ x → ≈⇒≋ (identityʳ x) + } + } + ; inverse = record + { fst = λ x → ≈⇒≋ (inverseˡ x) + ; snd = λ x → ≈⇒≋ (inverseʳ x) + } + ; ⁻¹-cong = ≋-⁻¹-cong + } + +quotientGroup : Group c (c ⊔ ℓ ⊔ c′) +quotientGroup = record { isGroup = quotientIsGroup } + +project : Group.Carrier G → Group.Carrier quotientGroup +project x = x -- because we do all the work in the relation + +project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project +project-isHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = ≈⇒≋ + } + ; homo = λ _ _ → ≋-refl + } + ; ε-homo = ≋-refl + } + ; ⁻¹-homo = λ _ → ≋-refl + } + +project-surjective : Surjective _≈_ _≋_ project +project-surjective g = g , ≈⇒≋ diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda new file mode 100644 index 0000000000..e45f305471 --- /dev/null +++ b/src/Algebra/NormalSubgroup.agda @@ -0,0 +1,28 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of normal subgroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) + +module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where + +open import Algebra.Construct.Sub.Group G using (Subgroup) +open import Data.Product.Base using (∃-syntax) +open import Level using (suc; _⊔_) + +private + module G = Group G + +record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + subgroup : Subgroup c′ ℓ′ + + open Subgroup subgroup public + + field + -- every element of N commutes in G + normal : ∀ n g → ∃[ n′ ] g G.∙ ι n G.≈ ι n′ G.∙ g From 694e0a5594bd2c6955bb1314e3c6fed88a6852fb Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 31 Oct 2025 07:54:38 +0100 Subject: [PATCH 02/12] Factor out Normal, show abelian implies subgroup is normal --- src/Algebra/NormalSubgroup.agda | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index e45f305471..5e5d508175 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -10,19 +10,26 @@ open import Algebra.Bundles using (Group) module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where +open import Algebra.Definitions open import Algebra.Construct.Sub.Group G using (Subgroup) -open import Data.Product.Base using (∃-syntax) +open import Data.Product.Base using (∃-syntax; _,_) open import Level using (suc; _⊔_) private module G = Group G +-- every element of the subgroup commutes in G +Normal : ∀ {c′ ℓ′} → Subgroup c′ ℓ′ → Set (c ⊔ ℓ ⊔ c′) +Normal subgroup = ∀ n g → ∃[ n′ ] g G.∙ ι n G.≈ ι n′ G.∙ g + where open Subgroup subgroup + record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field subgroup : Subgroup c′ ℓ′ + normal : Normal subgroup open Subgroup subgroup public - field - -- every element of N commutes in G - normal : ∀ n g → ∃[ n′ ] g G.∙ ι n G.≈ ι n′ G.∙ g +abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → Normal subgroup +abelian⇒subgroup-normal ∙-comm subgroup n g = n , ∙-comm g (ι n) + where open Subgroup subgroup From 52c3f807eb7fbb6976645e38e0d76d63d2f57280 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 31 Oct 2025 08:01:19 +0100 Subject: [PATCH 03/12] Use symmetric form of normality I noted that every time I used normal it was under sym This felt like a good reason to reverse it --- src/Algebra/Construct/Quotient/Group.agda | 5 ++--- src/Algebra/NormalSubgroup.agda | 4 ++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index ae9fda4644..0f8c674316 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -66,15 +66,14 @@ open AlgDefs _≋_ ≋-∙-cong : Congruent₂ _∙_ ≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩ - (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv∙wx≈u[vw∙x] (ι g) (ι h′) x u ⟩ - ι g ∙ ((ι h′ ∙ x) ∙ u) ≈⟨ uv≈w⇒xu∙v≈xw (uv≈w⇒u∙vx≈wx (normal h x .proj₂) u) (ι g) ⟨ + (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x .proj₂) (ι g) u ⟩ (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ y ∙ v ∎ where h′ = normal h x .proj₁ ≋-⁻¹-cong : Congruent₁ _⁻¹ ≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin - ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) .proj₂ ⟨ + ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) .proj₂ ⟩ x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩ x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨ (ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩ diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index 5e5d508175..2bcde22b5f 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -20,7 +20,7 @@ private -- every element of the subgroup commutes in G Normal : ∀ {c′ ℓ′} → Subgroup c′ ℓ′ → Set (c ⊔ ℓ ⊔ c′) -Normal subgroup = ∀ n g → ∃[ n′ ] g G.∙ ι n G.≈ ι n′ G.∙ g +Normal subgroup = ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n where open Subgroup subgroup record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where @@ -31,5 +31,5 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh open Subgroup subgroup public abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → Normal subgroup -abelian⇒subgroup-normal ∙-comm subgroup n g = n , ∙-comm g (ι n) +abelian⇒subgroup-normal ∙-comm subgroup n g = n , ∙-comm (ι n) g where open Subgroup subgroup From 057645cd7f5f2fec46bd5f9882d1d814cae3ef5b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 3 Nov 2025 09:49:28 +0100 Subject: [PATCH 04/12] Make Normal a record called IsNormal --- src/Algebra/NormalSubgroup.agda | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index 2bcde22b5f..c8a15afd0b 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -19,6 +19,11 @@ private module G = Group G -- every element of the subgroup commutes in G +record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where + open Subgroup subgroup + field + normal : ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n + Normal : ∀ {c′ ℓ′} → Subgroup c′ ℓ′ → Set (c ⊔ ℓ ⊔ c′) Normal subgroup = ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n where open Subgroup subgroup @@ -26,10 +31,11 @@ Normal subgroup = ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field subgroup : Subgroup c′ ℓ′ - normal : Normal subgroup + isNormal : IsNormal subgroup open Subgroup subgroup public + open IsNormal isNormal public -abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → Normal subgroup -abelian⇒subgroup-normal ∙-comm subgroup n g = n , ∙-comm (ι n) g +abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → IsNormal subgroup +abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → n , ∙-comm (ι n) g } where open Subgroup subgroup From 3c80fedb6eda11172bdc5ce5775d2fe4e9600ea3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 3 Nov 2025 10:14:27 +0100 Subject: [PATCH 05/12] Add _/_ synomym for quotient group --- src/Algebra/Construct/Quotient/Group.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 0f8c674316..e0d1ecdfdd 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -105,6 +105,9 @@ quotientIsGroup = record quotientGroup : Group c (c ⊔ ℓ ⊔ c′) quotientGroup = record { isGroup = quotientIsGroup } +_/_ : Group c (c ⊔ ℓ ⊔ c′) +_/_ = quotientGroup + project : Group.Carrier G → Group.Carrier quotientGroup project x = x -- because we do all the work in the relation From a9c134af784d21ff47afc86c4df60d7a6baa7576 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 3 Nov 2025 10:18:25 +0100 Subject: [PATCH 06/12] Remove old Normal definition --- src/Algebra/NormalSubgroup.agda | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index c8a15afd0b..ce35e2d891 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -24,10 +24,6 @@ record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ field normal : ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n -Normal : ∀ {c′ ℓ′} → Subgroup c′ ℓ′ → Set (c ⊔ ℓ ⊔ c′) -Normal subgroup = ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n - where open Subgroup subgroup - record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field subgroup : Subgroup c′ ℓ′ From 55aa35b5767b84da313718ff6add7fd1efc8a3d1 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 3 Nov 2025 10:22:21 +0100 Subject: [PATCH 07/12] Split product up into two fields in IsNormal --- src/Algebra/Construct/Quotient/Group.agda | 12 ++++++------ src/Algebra/NormalSubgroup.agda | 6 +++--- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index e0d1ecdfdd..f52a3c4486 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -18,7 +18,7 @@ open import Algebra.Morphism.Structures using (IsGroupHomomorphism) open import Algebra.Properties.Monoid monoid open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) open import Algebra.Structures using (IsGroup) -open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Product.Base using (_,_) open import Function.Definitions using (Surjective) open import Level using (_⊔_) open import Relation.Binary.Core using (_⇒_) @@ -28,7 +28,7 @@ open import Relation.Binary.Reasoning.Setoid setoid private module N = NormalSubgroup N -open NormalSubgroup N using (ι; module ι; normal) +open NormalSubgroup N using (ι; module ι; conjugate; normal) infix 0 _by_ @@ -66,19 +66,19 @@ open AlgDefs _≋_ ≋-∙-cong : Congruent₂ _∙_ ≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩ - (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x .proj₂) (ι g) u ⟩ + (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩ (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ y ∙ v ∎ - where h′ = normal h x .proj₁ + where h′ = conjugate h x ≋-⁻¹-cong : Congruent₁ _⁻¹ ≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin - ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) .proj₂ ⟩ + ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩ x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩ x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨ (ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩ y ⁻¹ ∎ - where h = normal (g N.⁻¹) (x ⁻¹) .proj₁ + where h = conjugate (g N.⁻¹) (x ⁻¹) quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹ quotientIsGroup = record diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index ce35e2d891..8fb7381fc5 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -12,7 +12,6 @@ module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where open import Algebra.Definitions open import Algebra.Construct.Sub.Group G using (Subgroup) -open import Data.Product.Base using (∃-syntax; _,_) open import Level using (suc; _⊔_) private @@ -22,7 +21,8 @@ private record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where open Subgroup subgroup field - normal : ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n + conjugate : ∀ n g → Carrier + normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field @@ -33,5 +33,5 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh open IsNormal isNormal public abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → IsNormal subgroup -abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → n , ∙-comm (ι n) g } +abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → ∙-comm (ι n) g } where open Subgroup subgroup From c4cea199287231de53067c6f2ca4e4be5aaa7994 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:52:50 +0100 Subject: [PATCH 08/12] Fix changelog typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index aab52c2691..8b481e31e4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,7 +79,7 @@ Deprecated names New modules ----------- -* `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups. +* `Algebra.Construct.Quotient.Group` for the definition of quotient groups. * `Algebra.Construct.Sub.Group` for the definition of subgroups. From 99401589fe2062322d9a31de3435ae65781db634 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:54:01 +0100 Subject: [PATCH 09/12] Explicitly import Commutative --- src/Algebra/NormalSubgroup.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/NormalSubgroup.agda b/src/Algebra/NormalSubgroup.agda index 8fb7381fc5..80240a85a0 100644 --- a/src/Algebra/NormalSubgroup.agda +++ b/src/Algebra/NormalSubgroup.agda @@ -10,7 +10,7 @@ open import Algebra.Bundles using (Group) module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where -open import Algebra.Definitions +open import Algebra.Definitions using (Commutative) open import Algebra.Construct.Sub.Group G using (Subgroup) open import Level using (suc; _⊔_) From d5c518bed2b391b57845b443e463fb76fbc3cde7 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:55:12 +0100 Subject: [PATCH 10/12] Define propositional reflexivity in terms of abstract reflexivity --- src/Algebra/Construct/Quotient/Group.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index f52a3c4486..485f366f73 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -35,8 +35,11 @@ infix 0 _by_ data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y +≈⇒≋ : _≈_ ⇒ _≋_ +≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y) + ≋-refl : Reflexive _≋_ -≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x) +≋-refl = ≈⇒≋ refl ≋-sym : Symmetric _≋_ ≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin @@ -58,9 +61,6 @@ data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where ; trans = ≋-trans } -≈⇒≋ : _≈_ ⇒ _≋_ -≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y) - open AlgDefs _≋_ ≋-∙-cong : Congruent₂ _∙_ From bf1acf9a1d0566f60aeb3f5612d9522dcb5c7125 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 11:32:10 +0100 Subject: [PATCH 11/12] Rename project to pi --- src/Algebra/Construct/Quotient/Group.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 485f366f73..6aebc25a0d 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -108,11 +108,11 @@ quotientGroup = record { isGroup = quotientIsGroup } _/_ : Group c (c ⊔ ℓ ⊔ c′) _/_ = quotientGroup -project : Group.Carrier G → Group.Carrier quotientGroup -project x = x -- because we do all the work in the relation +π : Group.Carrier G → Group.Carrier quotientGroup +π x = x -- because we do all the work in the relation -project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project -project-isHomomorphism = record +π-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π +π-isHomomorphism = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { isRelHomomorphism = record @@ -125,5 +125,5 @@ project-isHomomorphism = record ; ⁻¹-homo = λ _ → ≋-refl } -project-surjective : Surjective _≈_ _≋_ project -project-surjective g = g , ≈⇒≋ +π-surjective : Surjective _≈_ _≋_ π +π-surjective g = g , ≈⇒≋ From 0ecd8e072d08db7ed5617cf718d54936fe32f6f8 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 11:32:37 +0100 Subject: [PATCH 12/12] Use _,_ rather than record syntax --- src/Algebra/Construct/Quotient/Group.agda | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 6aebc25a0d..66fb3038b5 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -19,6 +19,7 @@ open import Algebra.Properties.Monoid monoid open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) open import Algebra.Structures using (IsGroup) open import Data.Product.Base using (_,_) +open import Function.Base using (_∘_) open import Function.Definitions using (Surjective) open import Level using (_⊔_) open import Relation.Binary.Core using (_⇒_) @@ -90,15 +91,9 @@ quotientIsGroup = record } ; assoc = λ x y z → ≈⇒≋ (assoc x y z) } - ; identity = record - { fst = λ x → ≈⇒≋ (identityˡ x) - ; snd = λ x → ≈⇒≋ (identityʳ x) - } - } - ; inverse = record - { fst = λ x → ≈⇒≋ (inverseˡ x) - ; snd = λ x → ≈⇒≋ (inverseʳ x) + ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ } + ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ ; ⁻¹-cong = ≋-⁻¹-cong }