From e2ff677ed39cf9336abc5cd81bb32aaf039ff310 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 14:10:20 +0000 Subject: [PATCH 01/25] refactor: alternative to #2852 and #2854 --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6679049fd0..3f3ad2178f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,6 +79,12 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups. + +* `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups. + +* `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups. + * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. From f702f82769122220fa79d7a2ac43666db136b169 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 14:12:53 +0000 Subject: [PATCH 02/25] refactor: alternative to #2852 and #2854 --- .../Construct/Quotient/AbelianGroup.agda | 35 +++++ src/Algebra/Construct/Quotient/Group.agda | 126 ++++++++++++++++++ src/Algebra/Construct/Sub/AbelianGroup.agda | 48 +++++++ src/Algebra/Construct/Sub/Group.agda | 31 +++++ src/Algebra/Construct/Sub/Group/Normal.agda | 32 +++++ 5 files changed, 272 insertions(+) create mode 100644 src/Algebra/Construct/Quotient/AbelianGroup.agda create mode 100644 src/Algebra/Construct/Quotient/Group.agda create mode 100644 src/Algebra/Construct/Sub/AbelianGroup.agda create mode 100644 src/Algebra/Construct/Sub/Group.agda create mode 100644 src/Algebra/Construct/Sub/Group/Normal.agda diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda new file mode 100644 index 0000000000..46ccdf3c68 --- /dev/null +++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda @@ -0,0 +1,35 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient Abelian groups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; AbelianGroup) +import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup + +module Algebra.Construct.Quotient.AbelianGroup + {c ℓ} (G : AbelianGroup c ℓ) + (open AbelianSubgroup G using (Subgroup; normalSubgroup)) + {c′ ℓ′} (N : Subgroup c′ ℓ′) + where + +private + module G = AbelianGroup G + +-- Re-export the quotient group + +open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public + +-- With its additional bundle + +quotientAbelianGroup : AbelianGroup c _ +quotientAbelianGroup = record + { isAbelianGroup = record + { isGroup = isGroup + ; comm = λ g h → ≈⇒≋ (G.comm g h) + } + } where open Group quotientGroup + +-- Public re-exports, as needed? diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda new file mode 100644 index 0000000000..99e22352cf --- /dev/null +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -0,0 +1,126 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient groups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) +open import Algebra.Construct.Sub.Group.Normal using (NormalSubgroup) + +module Algebra.Construct.Quotient.Group + {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where + +open import Algebra.Definitions using (Congruent₁; Congruent₂) +open import Algebra.Morphism.Structures + using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism) +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 (_⇒_) +open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) + +private + open module G = Group G + +open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) +open import Algebra.Properties.Monoid monoid +open import Relation.Binary.Reasoning.Setoid setoid + +private + open module N = NormalSubgroup N + using (ι; module ι; conjugate; normal) + +infix 0 _by_ + +data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where + _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y + +≈⇒≋ : _≈_ ⇒ _≋_ +≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _) + +≋-refl : Reflexive _≋_ +≋-refl = ≈⇒≋ refl + +≋-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 ∎ + +≋-∙-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) (ι g) u ⟩ + (ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩ + y ∙ v ∎ + where h′ = conjugate h x + +≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹ +≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin + ι 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 = conjugate (g N.⁻¹) (x ⁻¹) + +quotientGroup : Group c (c ⊔ ℓ ⊔ c′) +quotientGroup = record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = record + { refl = ≋-refl + ; sym = ≋-sym + ; trans = ≋-trans + } + ; ∙-cong = ≋-∙-cong + } + ; assoc = λ x y z → ≈⇒≋ (assoc x y z) + } + ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ + } + ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ + ; ⁻¹-cong = ≋-⁻¹-cong + } + } + +_/_ : Group c (c ⊔ ℓ ⊔ c′) +_/_ = quotientGroup + +π : Group.Carrier G → Group.Carrier quotientGroup +π x = x -- because we do all the work in the relation + +π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π +π-isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = ≈⇒≋ + } + ; homo = λ _ _ → ≋-refl + } + +π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π +π-isMonoidHomomorphism = record + { isMagmaHomomorphism = π-isMagmaHomomorphism + ; ε-homo = ≋-refl + } + +π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π +π-isGroupHomomorphism = record + { isMonoidHomomorphism = π-isMonoidHomomorphism + ; ⁻¹-homo = λ _ → ≋-refl + } + +π-surjective : Surjective _≈_ _≋_ π +π-surjective g = g , ≈⇒≋ diff --git a/src/Algebra/Construct/Sub/AbelianGroup.agda b/src/Algebra/Construct/Sub/AbelianGroup.agda new file mode 100644 index 0000000000..be527587cd --- /dev/null +++ b/src/Algebra/Construct/Sub/AbelianGroup.agda @@ -0,0 +1,48 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Subgroups of Abelian groups: necessarily Normal +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (AbelianGroup) + +module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where + +open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup) + +private + module G = AbelianGroup G + +open import Algebra.Construct.Sub.Group.Normal G.group + using (IsNormal; NormalSubgroup) + +-- Re-export the notion of subgroup of the underlying Group + +open import Algebra.Construct.Sub.Group G.group public + using (Subgroup) + +-- Then, for any such Subgroup: +-- * it defines an AbelianGroup +-- * and is, in fact, Normal + +module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where + + open Subgroup subgroup public + using (ι; ι-monomorphism) + + abelianGroup : AbelianGroup c′ ℓ′ + abelianGroup = record + { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup } + + open AbelianGroup abelianGroup public + + isNormal : IsNormal subgroup + isNormal = record { normal = λ n → G.comm (ι n) } + + normalSubgroup : NormalSubgroup c′ ℓ′ + normalSubgroup = record { isNormal = isNormal } + + open NormalSubgroup normalSubgroup public + using (conjugate; normal) diff --git a/src/Algebra/Construct/Sub/Group.agda b/src/Algebra/Construct/Sub/Group.agda new file mode 100644 index 0000000000..a43a2070de --- /dev/null +++ b/src/Algebra/Construct/Sub/Group.agda @@ -0,0 +1,31 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of subgroup via Group monomorphism +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; RawGroup) + +module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where + +open import Algebra.Morphism.Structures using (IsGroupMonomorphism) +open import Algebra.Morphism.GroupMonomorphism using (isGroup) +open import Level using (suc; _⊔_) + +private + module G = Group G + +record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + domain : RawGroup c′ ℓ′ + ι : _ → G.Carrier + ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι + + module ι = IsGroupMonomorphism ι-monomorphism + + group : Group _ _ + group = record { isGroup = isGroup ι-monomorphism G.isGroup } + + open Group group public diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda new file mode 100644 index 0000000000..4ff5f1d18c --- /dev/null +++ b/src/Algebra/Construct/Sub/Group/Normal.agda @@ -0,0 +1,32 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of normal subgroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group) + +module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ) where + +open import Algebra.Construct.Sub.Group G using (Subgroup) +open import Level using (suc; _⊔_) + +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 using (ι) + field + conjugate : ∀ n g → _ + normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n + +record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + subgroup : Subgroup c′ ℓ′ + isNormal : IsNormal subgroup + + open Subgroup subgroup public + open IsNormal isNormal public From bd5cfeed0b9073ca71959c0d6bb38d38a2e8a9da Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 14:27:23 +0000 Subject: [PATCH 03/25] add: sub-`Bimodule`s --- CHANGELOG.md | 2 + .../Module/Construct/Sub/Bimodule.agda | 53 +++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 src/Algebra/Module/Construct/Sub/Bimodule.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 3f3ad2178f..dd92156200 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -85,6 +85,8 @@ New modules * `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups. +* `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules. + * `Algebra.Properties.BooleanRing`. * `Algebra.Properties.BooleanSemiring`. diff --git a/src/Algebra/Module/Construct/Sub/Bimodule.agda b/src/Algebra/Module/Construct/Sub/Bimodule.agda new file mode 100644 index 0000000000..19c778a4bf --- /dev/null +++ b/src/Algebra/Module/Construct/Sub/Bimodule.agda @@ -0,0 +1,53 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of sub-bimodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Ring) +open import Algebra.Module.Bundles using (Bimodule; RawBimodule) + +module Algebra.Module.Construct.Sub.Bimodule + {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) + where + +open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism) +open import Algebra.Module.Morphism.BimoduleMonomorphism using (isBimodule) +open import Level using (suc; _⊔_) + +private + module R = Ring R + module S = Ring S + module M = Bimodule M + +open import Algebra.Construct.Sub.AbelianGroup M.+ᴹ-abelianGroup + as AbelianSubgroup + using (Subgroup) + +------------------------------------------------------------------------ +-- Definition + +record Subbimodule cm′ ℓm′ : Set (cr ⊔ cs ⊔ cm ⊔ ℓm ⊔ suc (cm′ ⊔ ℓm′)) where + field + domain : RawBimodule R.Carrier S.Carrier cm′ ℓm′ + ι : _ → M.Carrierᴹ + ι-monomorphism : IsBimoduleMonomorphism domain M.rawBimodule ι + + module ι = IsBimoduleMonomorphism ι-monomorphism + + bimodule : Bimodule R S _ _ + bimodule = record + { isBimodule = isBimodule ι-monomorphism R.isRing S.isRing M.isBimodule } + + open Bimodule bimodule public + +-- Additionally, have Abelian (hence: Normal) subgroups of M.+ᴹ-abelianGroup + + subgroup : Subgroup cm′ ℓm′ + subgroup = record { ι-monomorphism = ι.+ᴹ-isGroupMonomorphism } + + isNormal = AbelianSubgroup.isNormal subgroup + + normalSubgroup = AbelianSubgroup.normalSubgroup subgroup From d3d6797ac2aabc9bec33f0f5dc1548896c27fc0e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 14:31:13 +0000 Subject: [PATCH 04/25] fix: whitespace --- src/Algebra/Construct/Quotient/AbelianGroup.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda index 46ccdf3c68..25187d25c9 100644 --- a/src/Algebra/Construct/Quotient/AbelianGroup.agda +++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda @@ -11,7 +11,7 @@ import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup module Algebra.Construct.Quotient.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) - (open AbelianSubgroup G using (Subgroup; normalSubgroup)) + (open AbelianSubgroup G using (Subgroup; normalSubgroup)) {c′ ℓ′} (N : Subgroup c′ ℓ′) where From c05773b2d7afa038cda83132813771df13027fdb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 15:09:06 +0000 Subject: [PATCH 05/25] add: `Ideal`s and quotients of `Ring`s --- CHANGELOG.md | 2 + src/Algebra/Construct/Quotient/Ring.agda | 76 +++++++++++++++++++++++ src/Algebra/Construct/Sub/Ring/Ideal.agda | 26 ++++++++ 3 files changed, 104 insertions(+) create mode 100644 src/Algebra/Construct/Quotient/Ring.agda create mode 100644 src/Algebra/Construct/Sub/Ring/Ideal.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index dd92156200..403d274c0c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -85,6 +85,8 @@ New modules * `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups. +* `Algebra.Construct.Sub.Ring.Ideal` for the definition of ideals of a ring. + * `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules. * `Algebra.Properties.BooleanRing`. diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda new file mode 100644 index 0000000000..574f68c5ff --- /dev/null +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -0,0 +1,76 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Quotient rings +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (AbelianGroup; Ring; RawRing) +open import Algebra.Construct.Sub.Ring.Ideal using (Ideal) + +module Algebra.Construct.Quotient.Ring + {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) + where + +open import Algebra.Morphism.Structures using (IsRingHomomorphism) +open import Data.Product.Base using (_,_) +open import Function.Base using (_∘_) +open import Level using (_⊔_) + +import Algebra.Construct.Quotient.AbelianGroup as Quotient + +private + module R = Ring R + module I = Ideal I + module R/I = Quotient R.+-abelianGroup I.subgroup + + +open R/I public + using (_≋_; _by_; ≋-refl; ≈⇒≋ + ; quotientAbelianGroup + ; π; π-isMonoidHomomorphism; π-surjective + ) + +open import Algebra.Definitions _≋_ using (Congruent₂) + +≋-*-cong : Congruent₂ R._*_ +≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin + ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩ + ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩ + ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩ + ι j * ι k + ι j * u + x * ι k + x * u ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨ + (ι j + x) * (ι k + u) ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩ + y * v ∎ + where + open R using (_+_; _*_; +-congʳ ;+-cong; *-cong) + open import Algebra.Properties.Semiring R.semiring using (binomial-expansion) + open import Relation.Binary.Reasoning.Setoid R.setoid + open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_) + +quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′) +quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ } + +quotientRing : Ring c (c ⊔ ℓ ⊔ c′) +quotientRing = record + { isRing = record + { +-isAbelianGroup = isAbelianGroup + ; *-cong = ≋-*-cong + ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z) + ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ + ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z)) + } + } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup) + +π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π +π-isRingHomomorphism = record + { isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = π-isMonoidHomomorphism + ; *-homo = λ _ _ → ≋-refl + } + ; 1#-homo = ≋-refl + } + ; -‿homo = λ _ → ≋-refl + } + diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda new file mode 100644 index 0000000000..ceac1c1fb3 --- /dev/null +++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda @@ -0,0 +1,26 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ideals of a ring +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Ring) + +module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where + +open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule) +open import Algebra.Module.Construct.TensorUnit using (bimodule) +open import Level + +------------------------------------------------------------------------ +-- Definition +-- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself + +record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where + field + + subbimodule : Subbimodule {R = R} bimodule c′ ℓ′ + + open Subbimodule subbimodule public From b707d833c5d2d2e5fb9709ba1ad66f2be4791164 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 5 Nov 2025 15:14:39 +0000 Subject: [PATCH 06/25] fix: tidy up --- src/Algebra/Construct/Sub/Ring/Ideal.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Construct/Sub/Ring/Ideal.agda b/src/Algebra/Construct/Sub/Ring/Ideal.agda index ceac1c1fb3..8e40d0d7e1 100644 --- a/src/Algebra/Construct/Sub/Ring/Ideal.agda +++ b/src/Algebra/Construct/Sub/Ring/Ideal.agda @@ -12,7 +12,7 @@ module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule) open import Algebra.Module.Construct.TensorUnit using (bimodule) -open import Level +open import Level using (suc; _⊔_) ------------------------------------------------------------------------ -- Definition @@ -20,7 +20,6 @@ open import Level record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field - subbimodule : Subbimodule {R = R} bimodule c′ ℓ′ open Subbimodule subbimodule public From 7ad2b221d146ed3edbbd810d66b9cb156d722f6d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Nov 2025 15:54:57 +0000 Subject: [PATCH 07/25] add: `Center` of a `Group` --- CHANGELOG.md | 2 + src/Algebra/Construct/Centre/Group.agda | 101 ++++++++++++++++++++++++ 2 files changed, 103 insertions(+) create mode 100644 src/Algebra/Construct/Centre/Group.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 403d274c0c..963fea24cd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,6 +79,8 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Centre.Group` for the definition of the centre of a group. + * `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups. * `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups. diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda new file mode 100644 index 0000000000..34efd3b52d --- /dev/null +++ b/src/Algebra/Construct/Centre/Group.agda @@ -0,0 +1,101 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Group +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Group; RawGroup) + +module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where + +open import Algebra.Core using (Op₁; Op₂) +open import Function.Base using (id; _on_) +open import Level using (_⊔_) +open import Relation.Unary using (Pred) +open import Relation.Binary.Core using (Rel) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra.Construct.Sub.Group G using (Subgroup) +open import Algebra.Properties.Group G using (∙-cancelʳ) + +private + module G = Group G + +CommutesWith : Pred G.Carrier _ +CommutesWith g = ∀ k → g G.∙ k G.≈ k G.∙ g + +private + open ≈-Reasoning G.setoid + + record Carrier : Set (c ⊔ ℓ) where + field + commuter : G.Carrier + commutes : CommutesWith commuter + + open Carrier using (commuter; commutes) + + _≈_ : Rel Carrier _ + _≈_ = G._≈_ on commuter + + _∙_ : Op₂ Carrier + g ∙ h = record + { commuter = commuter g G.∙ commuter h + ; commutes = λ k → begin + (commuter g G.∙ commuter h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ + commuter g G.∙ (commuter h G.∙ k) ≈⟨ G.∙-congˡ (commutes h k) ⟩ + commuter g G.∙ (k G.∙ commuter h) ≈⟨ G.assoc _ _ _ ⟨ + commuter g G.∙ k G.∙ commuter h ≈⟨ G.∙-congʳ (commutes g k) ⟩ + k G.∙ commuter g G.∙ commuter h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (commuter g G.∙ commuter h) ∎ + } + + ε : Carrier + ε = record + { commuter = G.ε + ; commutes = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) + } + + _⁻¹ : Op₁ Carrier + g ⁻¹ = record + { commuter = commuter g G.⁻¹ + ; commutes = λ k → ∙-cancelʳ (commuter g) _ _ (begin + (commuter g G.⁻¹ G.∙ k) G.∙ (commuter g) ≈⟨ G.assoc _ _ _ ⟩ + commuter g G.⁻¹ G.∙ (k G.∙ commuter g) ≈⟨ G.∙-congˡ (commutes g k) ⟨ + commuter g G.⁻¹ G.∙ (commuter g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ + (commuter g G.⁻¹ G.∙ commuter g) G.∙ k ≈⟨ G.∙-congʳ (G.inverseˡ _) ⟩ + G.ε G.∙ k ≈⟨ commutes ε k ⟩ + k G.∙ G.ε ≈⟨ G.∙-congˡ (G.inverseˡ _) ⟨ + k G.∙ (commuter g G.⁻¹ G.∙ commuter g) ≈⟨ G.assoc _ _ _ ⟨ + (k G.∙ commuter g G.⁻¹) G.∙ (commuter g) ∎) + } + + +centre : Subgroup _ _ +centre = record + { domain = record + { _≈_ = _≈_ + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + } + ; ι = commuter + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → G.refl + } + ; ε-homo = G.refl + } + ; ⁻¹-homo = λ _ → G.refl + } + ; injective = id + } + } + +open Subgroup centre public + +Z[_] = group From b50f1d198bed75a1de46d10ed882497918d0d18b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Nov 2025 18:11:37 +0000 Subject: [PATCH 08/25] add: `Center` defines a `NormalSubgroup` --- src/Algebra/Construct/Centre/Group.agda | 80 +++++++++++++++---------- 1 file changed, 50 insertions(+), 30 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 34efd3b52d..e8a618a740 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -6,23 +6,26 @@ {-# OPTIONS --safe --cubical-compatible #-} -open import Algebra.Bundles using (Group; RawGroup) +open import Algebra.Bundles using (AbelianGroup; Group; RawGroup) module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where open import Algebra.Core using (Op₁; Op₂) -open import Function.Base using (id; _on_) +open import Algebra.Definitions using (Commutative) +open import Function.Base using (id; const; _$_; _on_) open import Level using (_⊔_) open import Relation.Unary using (Pred) open import Relation.Binary.Core using (Rel) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra.Construct.Sub.Group G using (Subgroup) +open import Algebra.Construct.Sub.Group.Normal G using (IsNormal; NormalSubgroup) open import Algebra.Properties.Group G using (∙-cancelʳ) private module G = Group G + CommutesWith : Pred G.Carrier _ CommutesWith g = ∀ k → g G.∙ k G.≈ k G.∙ g @@ -34,7 +37,7 @@ private commuter : G.Carrier commutes : CommutesWith commuter - open Carrier using (commuter; commutes) + open Carrier _≈_ : Rel Carrier _ _≈_ = G._≈_ on commuter @@ -44,9 +47,9 @@ private { commuter = commuter g G.∙ commuter h ; commutes = λ k → begin (commuter g G.∙ commuter h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ - commuter g G.∙ (commuter h G.∙ k) ≈⟨ G.∙-congˡ (commutes h k) ⟩ + commuter g G.∙ (commuter h G.∙ k) ≈⟨ G.∙-congˡ $ commutes h k ⟩ commuter g G.∙ (k G.∙ commuter h) ≈⟨ G.assoc _ _ _ ⟨ - commuter g G.∙ k G.∙ commuter h ≈⟨ G.∙-congʳ (commutes g k) ⟩ + commuter g G.∙ k G.∙ commuter h ≈⟨ G.∙-congʳ $ commutes g k ⟩ k G.∙ commuter g G.∙ commuter h ≈⟨ G.assoc _ _ _ ⟩ k G.∙ (commuter g G.∙ commuter h) ∎ } @@ -60,42 +63,59 @@ private _⁻¹ : Op₁ Carrier g ⁻¹ = record { commuter = commuter g G.⁻¹ - ; commutes = λ k → ∙-cancelʳ (commuter g) _ _ (begin + ; commutes = λ k → ∙-cancelʳ (commuter g) _ _ $ begin (commuter g G.⁻¹ G.∙ k) G.∙ (commuter g) ≈⟨ G.assoc _ _ _ ⟩ - commuter g G.⁻¹ G.∙ (k G.∙ commuter g) ≈⟨ G.∙-congˡ (commutes g k) ⟨ + commuter g G.⁻¹ G.∙ (k G.∙ commuter g) ≈⟨ G.∙-congˡ $ commutes g k ⟨ commuter g G.⁻¹ G.∙ (commuter g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ - (commuter g G.⁻¹ G.∙ commuter g) G.∙ k ≈⟨ G.∙-congʳ (G.inverseˡ _) ⟩ + (commuter g G.⁻¹ G.∙ commuter g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ G.ε G.∙ k ≈⟨ commutes ε k ⟩ - k G.∙ G.ε ≈⟨ G.∙-congˡ (G.inverseˡ _) ⟨ + k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ k G.∙ (commuter g G.⁻¹ G.∙ commuter g) ≈⟨ G.assoc _ _ _ ⟨ - (k G.∙ commuter g G.⁻¹) G.∙ (commuter g) ∎) + (k G.∙ commuter g G.⁻¹) G.∙ (commuter g) ∎ } + ∙-comm : Commutative _≈_ _∙_ + ∙-comm g h = commutes g $ commuter h + + +open Carrier public using (commuter; commutes) -centre : Subgroup _ _ +centre : NormalSubgroup _ _ centre = record - { domain = record - { _≈_ = _≈_ - ; _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = _⁻¹ - } - ; ι = commuter - ; ι-monomorphism = record - { isGroupHomomorphism = record - { isMonoidHomomorphism = record - { isMagmaHomomorphism = record - { isRelHomomorphism = record { cong = id } - ; homo = λ _ _ → G.refl - } - ; ε-homo = G.refl + { subgroup = record + { domain = record + { _≈_ = _≈_ + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + } + ; ι = commuter + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → G.refl + } + ; ε-homo = G.refl + } + ; ⁻¹-homo = λ _ → G.refl } - ; ⁻¹-homo = λ _ → G.refl + ; injective = id } - ; injective = id } + ; isNormal = record { conjugate = const ; normal = commutes } } -open Subgroup centre public +open NormalSubgroup centre public + +abelianGroup : AbelianGroup _ _ +abelianGroup = record + { + isAbelianGroup = record { isGroup = isGroup ; comm = ∙-comm } + } + +-- Public export + +Z[_] = centre -Z[_] = group From 78404b86136ab051584115a520568fd397da0a57 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 6 Nov 2025 22:53:51 +0000 Subject: [PATCH 09/25] refactor: make less visible! --- src/Algebra/Construct/Centre/Group.agda | 75 ++++++++++----------- src/Algebra/Construct/Sub/Group/Normal.agda | 2 +- 2 files changed, 37 insertions(+), 40 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index e8a618a740..72b0e3ecea 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -14,30 +14,27 @@ open import Algebra.Core using (Op₁; Op₂) open import Algebra.Definitions using (Commutative) open import Function.Base using (id; const; _$_; _on_) open import Level using (_⊔_) -open import Relation.Unary using (Pred) open import Relation.Binary.Core using (Rel) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra.Construct.Sub.Group G using (Subgroup) -open import Algebra.Construct.Sub.Group.Normal G using (IsNormal; NormalSubgroup) +open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup) open import Algebra.Properties.Group G using (∙-cancelʳ) +------------------------------------------------------------------------ +-- Definition + private module G = Group G - -CommutesWith : Pred G.Carrier _ -CommutesWith g = ∀ k → g G.∙ k G.≈ k G.∙ g - -private open ≈-Reasoning G.setoid record Carrier : Set (c ⊔ ℓ) where field commuter : G.Carrier - commutes : CommutesWith commuter + commutes : ∀ k → commuter G.∙ k G.≈ k G.∙ commuter - open Carrier + open Carrier using (commuter; commutes) _≈_ : Rel Carrier _ _≈_ = G._≈_ on commuter @@ -77,45 +74,45 @@ private ∙-comm : Commutative _≈_ _∙_ ∙-comm g h = commutes g $ commuter h - -open Carrier public using (commuter; commutes) - -centre : NormalSubgroup _ _ -centre = record - { subgroup = record - { domain = record - { _≈_ = _≈_ - ; _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = _⁻¹ - } - ; ι = commuter - ; ι-monomorphism = record - { isGroupHomomorphism = record - { isMonoidHomomorphism = record - { isMagmaHomomorphism = record - { isRelHomomorphism = record { cong = id } - ; homo = λ _ _ → G.refl + centre : NormalSubgroup _ _ + centre = record + { subgroup = record + { domain = record + { _≈_ = _≈_ + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + } + ; ι = commuter + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → G.refl + } + ; ε-homo = G.refl } - ; ε-homo = G.refl - } - ; ⁻¹-homo = λ _ → G.refl + ; ⁻¹-homo = λ _ → G.refl + } + ; injective = id } - ; injective = id } + ; isNormal = record { conjugate = const ; normal = commutes } } - ; isNormal = record { conjugate = const ; normal = commutes } - } + + +------------------------------------------------------------------------ +-- Public exports open NormalSubgroup centre public abelianGroup : AbelianGroup _ _ abelianGroup = record - { - isAbelianGroup = record { isGroup = isGroup ; comm = ∙-comm } + { isAbelianGroup = record + { isGroup = isGroup + ; comm = ∙-comm + } } --- Public export - Z[_] = centre - diff --git a/src/Algebra/Construct/Sub/Group/Normal.agda b/src/Algebra/Construct/Sub/Group/Normal.agda index 4ff5f1d18c..653bdba37a 100644 --- a/src/Algebra/Construct/Sub/Group/Normal.agda +++ b/src/Algebra/Construct/Sub/Group/Normal.agda @@ -8,7 +8,7 @@ open import Algebra.Bundles using (Group) -module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ) where +module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ) where open import Algebra.Construct.Sub.Group G using (Subgroup) open import Level using (suc; _⊔_) From e32165092b67180dfc45b0869eb58c0353d60e08 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 7 Nov 2025 06:38:48 +0000 Subject: [PATCH 10/25] fix: layout of `record`s --- src/Algebra/Construct/Centre/Group.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 72b0e3ecea..28f46487e8 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -98,7 +98,10 @@ private ; injective = id } } - ; isNormal = record { conjugate = const ; normal = commutes } + ; isNormal = record + { conjugate = const + ; normal = commutes + } } From c29e7d74102d2874c7ae3a4a459e4650a8ace718 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 8 Nov 2025 14:55:25 +0000 Subject: [PATCH 11/25] fix: tighten imports --- src/Algebra/Construct/Centre/Group.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 28f46487e8..a18f13ef7a 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -6,7 +6,7 @@ {-# OPTIONS --safe --cubical-compatible #-} -open import Algebra.Bundles using (AbelianGroup; Group; RawGroup) +open import Algebra.Bundles using (AbelianGroup; Group) module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where @@ -36,7 +36,7 @@ private open Carrier using (commuter; commutes) - _≈_ : Rel Carrier _ + _≈_ : Rel Carrier ℓ _≈_ = G._≈_ on commuter _∙_ : Op₂ Carrier @@ -74,7 +74,7 @@ private ∙-comm : Commutative _≈_ _∙_ ∙-comm g h = commutes g $ commuter h - centre : NormalSubgroup _ _ + centre : NormalSubgroup (c ⊔ ℓ) ℓ centre = record { subgroup = record { domain = record @@ -110,7 +110,7 @@ private open NormalSubgroup centre public -abelianGroup : AbelianGroup _ _ +abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup From b9e725afd8a85bc83291832242c5ef9c873f08f3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 9 Nov 2025 20:37:51 +0000 Subject: [PATCH 12/25] refactor: simplify throughout, making clear the relationship with `NormalSubgroup` --- src/Algebra/Construct/Centre/Group.agda | 74 +++++++++++-------------- 1 file changed, 32 insertions(+), 42 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index a18f13ef7a..650afe6318 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -11,13 +11,10 @@ open import Algebra.Bundles using (AbelianGroup; Group) module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where open import Algebra.Core using (Op₁; Op₂) -open import Algebra.Definitions using (Commutative) -open import Function.Base using (id; const; _$_; _on_) +open import Function.Base using (id; _∘_; const; _$_; _on_) open import Level using (_⊔_) -open import Relation.Binary.Core using (Rel) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Algebra.Construct.Sub.Group G using (Subgroup) open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup) open import Algebra.Properties.Group G using (∙-cancelʳ) @@ -31,59 +28,52 @@ private record Carrier : Set (c ⊔ ℓ) where field - commuter : G.Carrier - commutes : ∀ k → commuter G.∙ k G.≈ k G.∙ commuter + ι : G.Carrier + normal : ∀ g → ι G.∙ g G.≈ g G.∙ ι - open Carrier using (commuter; commutes) - - _≈_ : Rel Carrier ℓ - _≈_ = G._≈_ on commuter + open Carrier using (ι; normal) _∙_ : Op₂ Carrier g ∙ h = record - { commuter = commuter g G.∙ commuter h - ; commutes = λ k → begin - (commuter g G.∙ commuter h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ - commuter g G.∙ (commuter h G.∙ k) ≈⟨ G.∙-congˡ $ commutes h k ⟩ - commuter g G.∙ (k G.∙ commuter h) ≈⟨ G.assoc _ _ _ ⟨ - commuter g G.∙ k G.∙ commuter h ≈⟨ G.∙-congʳ $ commutes g k ⟩ - k G.∙ commuter g G.∙ commuter h ≈⟨ G.assoc _ _ _ ⟩ - k G.∙ (commuter g G.∙ commuter h) ∎ + { ι = ι g G.∙ ι h + ; normal = λ k → begin + (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ + ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ normal h k ⟩ + ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ normal g k ⟩ + k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (ι g G.∙ ι h) ∎ } ε : Carrier ε = record - { commuter = G.ε - ; commutes = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) + { ι = G.ε + ; normal = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) } _⁻¹ : Op₁ Carrier g ⁻¹ = record - { commuter = commuter g G.⁻¹ - ; commutes = λ k → ∙-cancelʳ (commuter g) _ _ $ begin - (commuter g G.⁻¹ G.∙ k) G.∙ (commuter g) ≈⟨ G.assoc _ _ _ ⟩ - commuter g G.⁻¹ G.∙ (k G.∙ commuter g) ≈⟨ G.∙-congˡ $ commutes g k ⟨ - commuter g G.⁻¹ G.∙ (commuter g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ - (commuter g G.⁻¹ G.∙ commuter g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ - G.ε G.∙ k ≈⟨ commutes ε k ⟩ - k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ - k G.∙ (commuter g G.⁻¹ G.∙ commuter g) ≈⟨ G.assoc _ _ _ ⟨ - (k G.∙ commuter g G.⁻¹) G.∙ (commuter g) ∎ + { ι = ι g G.⁻¹ + ; normal = λ k → ∙-cancelʳ (ι g) _ _ $ begin + (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ + ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ normal g k ⟨ + ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ + (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ + G.ε G.∙ k ≈⟨ normal ε k ⟩ + k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ + k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ + (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ } - ∙-comm : Commutative _≈_ _∙_ - ∙-comm g h = commutes g $ commuter h - - centre : NormalSubgroup (c ⊔ ℓ) ℓ - centre = record + normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ + normalSubgroup = record { subgroup = record { domain = record - { _≈_ = _≈_ - ; _∙_ = _∙_ + { _∙_ = _∙_ ; ε = ε ; _⁻¹ = _⁻¹ } - ; ι = commuter + ; ι = ι ; ι-monomorphism = record { isGroupHomomorphism = record { isMonoidHomomorphism = record @@ -100,7 +90,7 @@ private } ; isNormal = record { conjugate = const - ; normal = commutes + ; normal = normal } } @@ -108,14 +98,14 @@ private ------------------------------------------------------------------------ -- Public exports -open NormalSubgroup centre public +open NormalSubgroup normalSubgroup public abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup - ; comm = ∙-comm + ; comm = λ g → normal g ∘ ι } } -Z[_] = centre +Z[_] = normalSubgroup From f09f35f3fcae1ef11b88dc2cda03057d5007b0be Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 10 Nov 2025 08:59:04 +0000 Subject: [PATCH 13/25] add: definition of `Central` --- src/Algebra/Definitions.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index e42958da4d..0578d8416b 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -53,6 +53,9 @@ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) LeftIdentity : A → Op₂ A → Set _ LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x +Central : A → Op₂ A → Set _ +Central x _∙_ = ∀ y → (x ∙ y) ≈ (y ∙ x) + RightIdentity : A → Op₂ A → Set _ RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x From 03c7324d451d086c7e44c3bcde49230f5fd44259 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 10 Nov 2025 09:06:48 +0000 Subject: [PATCH 14/25] refactor: use `Central`; tweak exports --- src/Algebra/Construct/Centre/Group.agda | 89 +++++++++++++------------ src/Algebra/Definitions.agda | 4 +- 2 files changed, 47 insertions(+), 46 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 650afe6318..cb2689fd72 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -11,6 +11,7 @@ open import Algebra.Bundles using (AbelianGroup; Group) module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where open import Algebra.Core using (Op₁; Op₂) +open import Algebra.Definitions using (Central) open import Function.Base using (id; _∘_; const; _$_; _on_) open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -26,77 +27,77 @@ private open ≈-Reasoning G.setoid - record Carrier : Set (c ⊔ ℓ) where + record Center : Set (c ⊔ ℓ) where field - ι : G.Carrier - normal : ∀ g → ι G.∙ g G.≈ g G.∙ ι + ι : G.Carrier + central : Central G._≈_ G._∙_ ι - open Carrier using (ι; normal) + open Center using (ι; central) - _∙_ : Op₂ Carrier + _∙_ : Op₂ Center g ∙ h = record { ι = ι g G.∙ ι h - ; normal = λ k → begin + ; central = λ k → begin (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ - ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ normal h k ⟩ + ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ - ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ normal g k ⟩ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ k G.∙ (ι g G.∙ ι h) ∎ } - ε : Carrier + ε : Center ε = record { ι = G.ε - ; normal = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) + ; central = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) } - _⁻¹ : Op₁ Carrier + _⁻¹ : Op₁ Center g ⁻¹ = record { ι = ι g G.⁻¹ - ; normal = λ k → ∙-cancelʳ (ι g) _ _ $ begin + ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ - ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ normal g k ⟨ + ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ central g k ⟨ ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ - G.ε G.∙ k ≈⟨ normal ε k ⟩ + G.ε G.∙ k ≈⟨ central ε k ⟩ k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ } - normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ - normalSubgroup = record - { subgroup = record - { domain = record - { _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = _⁻¹ - } - ; ι = ι - ; ι-monomorphism = record - { isGroupHomomorphism = record - { isMonoidHomomorphism = record - { isMagmaHomomorphism = record - { isRelHomomorphism = record { cong = id } - ; homo = λ _ _ → G.refl - } - ; ε-homo = G.refl + +------------------------------------------------------------------------ +-- Public exports + +normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ +normalSubgroup = record + { subgroup = record + { domain = record + { _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + } + ; ι = ι + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → G.refl } - ; ⁻¹-homo = λ _ → G.refl - } - ; injective = id + ; ε-homo = G.refl + } + ; ⁻¹-homo = λ _ → G.refl } - } - ; isNormal = record - { conjugate = const - ; normal = normal + ; injective = id } } - - ------------------------------------------------------------------------- --- Public exports + ; isNormal = record + { conjugate = const + ; normal = central + } + } open NormalSubgroup normalSubgroup public @@ -104,8 +105,8 @@ abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup - ; comm = λ g → normal g ∘ ι + ; comm = λ g → central g ∘ ι } } -Z[_] = normalSubgroup +Z[_] = abelianGroup diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 0578d8416b..d210052c9b 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -53,8 +53,8 @@ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) LeftIdentity : A → Op₂ A → Set _ LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x -Central : A → Op₂ A → Set _ -Central x _∙_ = ∀ y → (x ∙ y) ≈ (y ∙ x) +Central : Op₂ A → A → Set _ +Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x) RightIdentity : A → Op₂ A → Set _ RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x From cc09919aab45630277a95e73a50cf4bea429ecac Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 10 Nov 2025 09:28:30 +0000 Subject: [PATCH 15/25] add: `Semigroup` --- src/Algebra/Construct/Centre/Semigroup.agda | 91 +++++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 src/Algebra/Construct/Centre/Semigroup.agda diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda new file mode 100644 index 0000000000..958bd592a9 --- /dev/null +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -0,0 +1,91 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Group +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (CommutativeSemigroup; Semigroup) + +module Algebra.Construct.Centre.Semigroup {c ℓ} (G : Semigroup c ℓ) where + +open import Algebra.Core using (Op₁; Op₂) +open import Algebra.Definitions using (Central) +open import Function.Base using (id; _∘_; const; _$_; _on_) +open import Level using (_⊔_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + + +------------------------------------------------------------------------ +-- Definition + +private + module G = Semigroup G + + open ≈-Reasoning G.setoid + + record Center : Set (c ⊔ ℓ) where + field + ι : G.Carrier + central : Central G._≈_ G._∙_ ι + + open Center using (ι; central) + + _∙_ : Op₂ Center + g ∙ h = record + { ι = ι g G.∙ ι h + ; central = λ k → begin + (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ + ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ + ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ + k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (ι g G.∙ ι h) ∎ + } + +{- +------------------------------------------------------------------------ +-- Public exports + +normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ +normalSubgroup = record + { subgroup = record + { domain = record + { _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + } + ; ι = ι + ; ι-monomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → G.refl + } + ; ε-homo = G.refl + } + ; ⁻¹-homo = λ _ → G.refl + } + ; injective = id + } + } + ; isNormal = record + { conjugate = const + ; normal = central + } + } + +open NormalSubgroup normalSubgroup public + +commutativeSemigroup : CommutativeSemigroup (c ⊔ ℓ) ℓ +commutativeSemigroup = record + { isCommutativeSemigroup = record + { isSemigroup = isSemigroup + ; comm = λ g → central g ∘ ι + } + } + +Z[_] = commutativeSemigroup +-} From a34d9dc648ee042b33332d06e9831d4c1cb2f5b1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Nov 2025 08:49:21 +0000 Subject: [PATCH 16/25] add: `Magma` and `Monoid` --- src/Algebra/Construct/Centre/Magma.agda | 44 +++++++++++++++ src/Algebra/Construct/Centre/Monoid.agda | 70 ++++++++++++++++++++++++ 2 files changed, 114 insertions(+) create mode 100644 src/Algebra/Construct/Centre/Magma.agda create mode 100644 src/Algebra/Construct/Centre/Monoid.agda diff --git a/src/Algebra/Construct/Centre/Magma.agda b/src/Algebra/Construct/Centre/Magma.agda new file mode 100644 index 0000000000..945ab12358 --- /dev/null +++ b/src/Algebra/Construct/Centre/Magma.agda @@ -0,0 +1,44 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Magma +-- +-- NB this doesn't make sense a priori, because in the absence of +-- associativity, it's not possible to define even a Magma operation +-- on the Center type defined below, as underlying Carrier. +-- +-- Yet a Magma *is* sufficient to define such a type, and thus can be +-- inherited up through the whole `Algebra.Construct.Centre.X` hierarchy. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles using (Magma) + +module Algebra.Construct.Centre.Magma {c ℓ} (G : Magma c ℓ) where + +open import Algebra.Definitions using (Central) +open import Function.Base using (id; _on_) +open import Level using (_⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) + +private + module G = Magma G + + +------------------------------------------------------------------------ +-- Definition + +record Center : Set (c ⊔ ℓ) where + field + ι : G.Carrier + central : Central G._≈_ G._∙_ ι + +open Center public + +_≈_ : Rel Center _ +_≈_ = G._≈_ on ι + +ι-isRelHomomorphism : IsRelHomomorphism _≈_ G._≈_ ι +ι-isRelHomomorphism = record { cong = id } diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda new file mode 100644 index 0000000000..aba06b403b --- /dev/null +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -0,0 +1,70 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Group +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (CommutativeMonoid; Monoid; RawMonoid; RawMagma) + +module Algebra.Construct.Centre.Monoid {c ℓ} (G : Monoid c ℓ) where + +open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) +open import Function.Base using (id; _∘_) + +import Algebra.Construct.Centre.Semigroup as Centre +open import Algebra.Construct.Sub.Monoid G using (Submonoid) + +private + module G = Monoid G + module Z = Centre G.semigroup + + +------------------------------------------------------------------------ +-- Definition + +open Z public + using (Center; ι; central) + +ε : Center +ε = record + { ι = G.ε + ; central = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) + } + +domain : RawMonoid _ _ +domain = record { RawMagma Z.domain ; ε = ε } + +ι-isMonoidHomomorphism : IsMonoidHomomorphism domain _ _ +ι-isMonoidHomomorphism = record + { isMagmaHomomorphism = Z.ι-isMagmaHomomorphism + ; ε-homo = G.refl + } + + +------------------------------------------------------------------------ +-- Public exports + +monoid : Monoid _ _ +monoid = Submonoid.monoid record + { domain = domain + ; ι = ι + ; ι-monomorphism = record + { isMonoidHomomorphism = ι-isMonoidHomomorphism + ; injective = id + } + } + +commutativeMonoid : CommutativeMonoid _ _ +commutativeMonoid = record + { isCommutativeMonoid = record + { isMonoid = isMonoid + ; comm = λ g → central g ∘ ι + } + } + where open Monoid monoid using (isMonoid) + +Z[_] = commutativeMonoid + From 6acb547c0951df457a1858af4d3fff14834e1579 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Nov 2025 08:49:58 +0000 Subject: [PATCH 17/25] refactor: via the hierarchy --- src/Algebra/Construct/Centre/Group.agda | 101 ++++++++------------ src/Algebra/Construct/Centre/Monoid.agda | 2 +- src/Algebra/Construct/Centre/Semigroup.agda | 97 ++++++++----------- 3 files changed, 81 insertions(+), 119 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index cb2689fd72..4d2cc11203 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -6,65 +6,53 @@ {-# OPTIONS --safe --cubical-compatible #-} -open import Algebra.Bundles using (AbelianGroup; Group) +open import Algebra.Bundles using (AbelianGroup; Group; RawGroup; RawMonoid) module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where -open import Algebra.Core using (Op₁; Op₂) -open import Algebra.Definitions using (Central) -open import Function.Base using (id; _∘_; const; _$_; _on_) +import Algebra.Construct.Centre.Monoid as Centre +open import Algebra.Core using (Op₁) +open import Algebra.Morphism.Structures using (IsGroupHomomorphism) +open import Function.Base using (id; _∘_; const; _$_) open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup) open import Algebra.Properties.Group G using (∙-cancelʳ) ------------------------------------------------------------------------- --- Definition - private module G = Group G + module Z = Centre G.monoid - open ≈-Reasoning G.setoid - - record Center : Set (c ⊔ ℓ) where - field - ι : G.Carrier - central : Central G._≈_ G._∙_ ι - - open Center using (ι; central) - - _∙_ : Op₂ Center - g ∙ h = record - { ι = ι g G.∙ ι h - ; central = λ k → begin - (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ - ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ - ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ - ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ - k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ - k G.∙ (ι g G.∙ ι h) ∎ - } - ε : Center - ε = record - { ι = G.ε - ; central = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k)) - } +------------------------------------------------------------------------ +-- Definition - _⁻¹ : Op₁ Center - g ⁻¹ = record - { ι = ι g G.⁻¹ - ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin - (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ - ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ central g k ⟨ - ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ - (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ - G.ε G.∙ k ≈⟨ central ε k ⟩ - k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ - k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ - (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ - } +open Z public + using (Center; ι; central) + +_⁻¹ : Op₁ Center +g ⁻¹ = record + { ι = ι g G.⁻¹ + ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin + (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ + ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ central g k ⟨ + ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ + (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ + G.ε G.∙ k ≈⟨ central Z.ε k ⟩ + k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ + k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ + (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ + } where open ≈-Reasoning G.setoid + +domain : RawGroup _ _ +domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } + +ι-isGroupHomomorphism : IsGroupHomomorphism domain _ _ +ι-isGroupHomomorphism = record + { isMonoidHomomorphism = Z.ι-isMonoidHomomorphism + ; ⁻¹-homo = λ _ → G.refl + } ------------------------------------------------------------------------ @@ -73,33 +61,21 @@ private normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ normalSubgroup = record { subgroup = record - { domain = record - { _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = _⁻¹ - } + { domain = domain ; ι = ι ; ι-monomorphism = record - { isGroupHomomorphism = record - { isMonoidHomomorphism = record - { isMagmaHomomorphism = record - { isRelHomomorphism = record { cong = id } - ; homo = λ _ _ → G.refl - } - ; ε-homo = G.refl - } - ; ⁻¹-homo = λ _ → G.refl + { isGroupHomomorphism = ι-isGroupHomomorphism + ; injective = id } - ; injective = id - } } ; isNormal = record { conjugate = const ; normal = central } } - +{- open NormalSubgroup normalSubgroup public + hiding (_⁻¹) abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record @@ -110,3 +86,4 @@ abelianGroup = record } Z[_] = abelianGroup +-} diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index aba06b403b..9561a8cbe2 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -27,7 +27,7 @@ private open Z public using (Center; ι; central) - + ε : Center ε = record { ι = G.ε diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 958bd592a9..3cb6e61417 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -6,86 +6,71 @@ {-# OPTIONS --safe --cubical-compatible #-} -open import Algebra.Bundles using (CommutativeSemigroup; Semigroup) +open import Algebra.Bundles using (CommutativeSemigroup; Semigroup; RawMagma) module Algebra.Construct.Centre.Semigroup {c ℓ} (G : Semigroup c ℓ) where -open import Algebra.Core using (Op₁; Op₂) -open import Algebra.Definitions using (Central) +import Algebra.Construct.Centre.Magma as Centre +open import Algebra.Core using (Op₂) +open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) open import Function.Base using (id; _∘_; const; _$_; _on_) open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Algebra.Construct.Sub.Semigroup G as Subsemigroup + +private + module G = Semigroup G + module Z = Centre G.magma + ------------------------------------------------------------------------ -- Definition -private - module G = Semigroup G +open Z public + using (Center; ι; central) + +_∙_ : Op₂ Center +ι (g ∙ h) = ι g G.∙ ι h +central (g ∙ h) = λ k → begin + (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ + ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ + ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ + k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (ι g G.∙ ι h) ∎ + where open ≈-Reasoning G.setoid + +domain : RawMagma _ _ +domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } + +ι-isMagmaHomomorphism : IsMagmaHomomorphism domain G.rawMagma ι +ι-isMagmaHomomorphism = record + { isRelHomomorphism = Z.ι-isRelHomomorphism + ; homo = λ _ _ → G.refl + } - open ≈-Reasoning G.setoid - - record Center : Set (c ⊔ ℓ) where - field - ι : G.Carrier - central : Central G._≈_ G._∙_ ι - - open Center using (ι; central) - - _∙_ : Op₂ Center - g ∙ h = record - { ι = ι g G.∙ ι h - ; central = λ k → begin - (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩ - ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩ - ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ - ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ central g k ⟩ - k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ - k G.∙ (ι g G.∙ ι h) ∎ - } -{- ------------------------------------------------------------------------ -- Public exports -normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ -normalSubgroup = record - { subgroup = record - { domain = record - { _∙_ = _∙_ - ; ε = ε - ; _⁻¹ = _⁻¹ - } - ; ι = ι - ; ι-monomorphism = record - { isGroupHomomorphism = record - { isMonoidHomomorphism = record - { isMagmaHomomorphism = record - { isRelHomomorphism = record { cong = id } - ; homo = λ _ _ → G.refl - } - ; ε-homo = G.refl - } - ; ⁻¹-homo = λ _ → G.refl - } - ; injective = id - } - } - ; isNormal = record - { conjugate = const - ; normal = central +semigroup : Semigroup _ _ +semigroup = Subsemigroup.semigroup record + { domain = domain + ; ι = ι + ; ι-monomorphism = record + { isMagmaHomomorphism = ι-isMagmaHomomorphism + ; injective = id } } -open NormalSubgroup normalSubgroup public - -commutativeSemigroup : CommutativeSemigroup (c ⊔ ℓ) ℓ +commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = record { isSemigroup = isSemigroup ; comm = λ g → central g ∘ ι } } + where open Semigroup semigroup using (isSemigroup) Z[_] = commutativeSemigroup --} From bd7f7ca7f9a14cd06d9150befa7b3a434ecae4b1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 11 Nov 2025 09:04:40 +0000 Subject: [PATCH 18/25] tidy up --- src/Algebra/Construct/Centre/Group.agda | 4 +--- src/Algebra/Construct/Centre/Monoid.agda | 4 +--- src/Algebra/Construct/Centre/Semigroup.agda | 4 +--- 3 files changed, 3 insertions(+), 9 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 4d2cc11203..a6c727f8db 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -61,9 +61,7 @@ domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ normalSubgroup = record { subgroup = record - { domain = domain - ; ι = ι - ; ι-monomorphism = record + { ι-monomorphism = record { isGroupHomomorphism = ι-isGroupHomomorphism ; injective = id } diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index 9561a8cbe2..dd06d5b363 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -49,9 +49,7 @@ domain = record { RawMagma Z.domain ; ε = ε } monoid : Monoid _ _ monoid = Submonoid.monoid record - { domain = domain - ; ι = ι - ; ι-monomorphism = record + { ι-monomorphism = record { isMonoidHomomorphism = ι-isMonoidHomomorphism ; injective = id } diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 3cb6e61417..4e7465ae8a 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -56,9 +56,7 @@ domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } semigroup : Semigroup _ _ semigroup = Subsemigroup.semigroup record - { domain = domain - ; ι = ι - ; ι-monomorphism = record + { ι-monomorphism = record { isMagmaHomomorphism = ι-isMagmaHomomorphism ; injective = id } From 9eb49f10500ee1ce161ee328542236504aaf4ca7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 06:56:57 +0000 Subject: [PATCH 19/25] fix: `Quotient`s by appropriate objects --- src/Algebra/Construct/Quotient/AbelianGroup.agda | 2 +- src/Algebra/Construct/Quotient/Group.agda | 2 +- src/Algebra/Construct/Quotient/Ring.agda | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Construct/Quotient/AbelianGroup.agda b/src/Algebra/Construct/Quotient/AbelianGroup.agda index 25187d25c9..c81cdf0952 100644 --- a/src/Algebra/Construct/Quotient/AbelianGroup.agda +++ b/src/Algebra/Construct/Quotient/AbelianGroup.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Quotient Abelian groups +-- Quotient of an Abelian group by a subgroup ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Construct/Quotient/Group.agda b/src/Algebra/Construct/Quotient/Group.agda index 99e22352cf..9f018deb40 100644 --- a/src/Algebra/Construct/Quotient/Group.agda +++ b/src/Algebra/Construct/Quotient/Group.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Quotient groups +-- Quotient of a Group by a NormalSubgroup ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda index 574f68c5ff..10ff1c8f34 100644 --- a/src/Algebra/Construct/Quotient/Ring.agda +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Quotient rings +-- Quotient of a Ring by an Ideal ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} From 806b220a0707e6e750f14edcc394e23f74379f33 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 07:06:01 +0000 Subject: [PATCH 20/25] fix: improve import/export? --- src/Algebra/Construct/Centre/Group.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index a6c727f8db..7153dc1d38 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -71,17 +71,17 @@ normalSubgroup = record ; normal = central } } -{- + open NormalSubgroup normalSubgroup public - hiding (_⁻¹) + hiding (domain; _⁻¹) abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup - ; comm = λ g → central g ∘ ι + ; comm = λ g → central g ∘ Z.ι } } Z[_] = abelianGroup --} + From 2222d281b1b269c7a038301e71642b16ee6305bb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 08:39:01 +0000 Subject: [PATCH 21/25] =?UTF-8?q?fix:=20improve=20export=20structure;=20is?= =?UTF-8?q?olate=20`=E2=88=99-comm`=20at=20the=20bootom=20of=20the=20hiera?= =?UTF-8?q?rchy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Construct/Centre/Group.agda | 25 ++++++++-------- src/Algebra/Construct/Centre/Magma.agda | 12 +++++++- src/Algebra/Construct/Centre/Monoid.agda | 27 ++++++++--------- src/Algebra/Construct/Centre/Semigroup.agda | 32 +++++++++++++-------- 4 files changed, 57 insertions(+), 39 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 7153dc1d38..b0cb99630d 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -12,7 +12,7 @@ module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where import Algebra.Construct.Centre.Monoid as Centre open import Algebra.Core using (Op₁) -open import Algebra.Morphism.Structures using (IsGroupHomomorphism) +open import Algebra.Morphism.Structures using (IsGroupMonomorphism) open import Function.Base using (id; _∘_; const; _$_) open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -29,7 +29,8 @@ private -- Definition open Z public - using (Center; ι; central) + using (Center; ι; central; ∙-comm) + hiding (module ι) _⁻¹ : Op₁ Center g ⁻¹ = record @@ -48,10 +49,13 @@ g ⁻¹ = record domain : RawGroup _ _ domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } -ι-isGroupHomomorphism : IsGroupHomomorphism domain _ _ -ι-isGroupHomomorphism = record - { isMonoidHomomorphism = Z.ι-isMonoidHomomorphism - ; ⁻¹-homo = λ _ → G.refl +ι-isGroupMonomorphism : IsGroupMonomorphism domain _ _ +ι-isGroupMonomorphism = record + { isGroupHomomorphism = record + { isMonoidHomomorphism = Z.ι.isMonoidHomomorphism + ; ⁻¹-homo = λ _ → G.refl + } + ; injective = id } @@ -60,12 +64,7 @@ domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ normalSubgroup = record - { subgroup = record - { ι-monomorphism = record - { isGroupHomomorphism = ι-isGroupHomomorphism - ; injective = id - } - } + { subgroup = record { ι-monomorphism = ι-isGroupMonomorphism } ; isNormal = record { conjugate = const ; normal = central @@ -79,7 +78,7 @@ abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup - ; comm = λ g → central g ∘ Z.ι + ; comm = ∙-comm } } diff --git a/src/Algebra/Construct/Centre/Magma.agda b/src/Algebra/Construct/Centre/Magma.agda index 945ab12358..efa1c68502 100644 --- a/src/Algebra/Construct/Centre/Magma.agda +++ b/src/Algebra/Construct/Centre/Magma.agda @@ -17,11 +17,13 @@ open import Algebra.Bundles using (Magma) module Algebra.Construct.Centre.Magma {c ℓ} (G : Magma c ℓ) where +open import Algebra.Core using (Op₂) open import Algebra.Definitions using (Central) open import Function.Base using (id; _on_) open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) +open import Relation.Binary.Morphism.Structures + using (IsRelHomomorphism; IsRelMonomorphism) private module G = Magma G @@ -42,3 +44,11 @@ _≈_ = G._≈_ on ι ι-isRelHomomorphism : IsRelHomomorphism _≈_ G._≈_ ι ι-isRelHomomorphism = record { cong = id } + +ι-isRelMonomorphism : IsRelMonomorphism _≈_ G._≈_ ι +ι-isRelMonomorphism = record + { isHomomorphism = ι-isRelHomomorphism + ; injective = id + } + +module ι = IsRelMonomorphism ι-isRelMonomorphism diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index dd06d5b363..868bc8238f 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -11,7 +11,7 @@ open import Algebra.Bundles module Algebra.Construct.Centre.Monoid {c ℓ} (G : Monoid c ℓ) where -open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) +open import Algebra.Morphism.Structures using (IsMonoidMonomorphism) open import Function.Base using (id; _∘_) import Algebra.Construct.Centre.Semigroup as Centre @@ -26,7 +26,8 @@ private -- Definition open Z public - using (Center; ι; central) + using (Center; ι; central; ∙-comm) + hiding (module ι) ε : Center ε = record @@ -37,29 +38,29 @@ open Z public domain : RawMonoid _ _ domain = record { RawMagma Z.domain ; ε = ε } -ι-isMonoidHomomorphism : IsMonoidHomomorphism domain _ _ -ι-isMonoidHomomorphism = record - { isMagmaHomomorphism = Z.ι-isMagmaHomomorphism - ; ε-homo = G.refl +ι-isMonoidMonomorphism : IsMonoidMonomorphism domain _ _ +ι-isMonoidMonomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = Z.ι.isMagmaHomomorphism + ; ε-homo = G.refl + } + ; injective = id } +module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism + ------------------------------------------------------------------------ -- Public exports monoid : Monoid _ _ -monoid = Submonoid.monoid record - { ι-monomorphism = record - { isMonoidHomomorphism = ι-isMonoidHomomorphism - ; injective = id - } - } +monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism } commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = record { isMonoid = isMonoid - ; comm = λ g → central g ∘ ι + ; comm = ∙-comm } } where open Monoid monoid using (isMonoid) diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 4e7465ae8a..6f1c897cc7 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -12,7 +12,8 @@ module Algebra.Construct.Centre.Semigroup {c ℓ} (G : Semigroup c ℓ) where import Algebra.Construct.Centre.Magma as Centre open import Algebra.Core using (Op₂) -open import Algebra.Morphism.Structures using (IsMagmaHomomorphism) +open import Algebra.Definitions using (Commutative) +open import Algebra.Morphism.Structures using (IsMagmaMonomorphism) open import Function.Base using (id; _∘_; const; _$_; _on_) open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -29,6 +30,7 @@ private open Z public using (Center; ι; central) + hiding (module ι) _∙_ : Op₂ Center ι (g ∙ h) = ι g G.∙ ι h @@ -41,32 +43,38 @@ central (g ∙ h) = λ k → begin k G.∙ (ι g G.∙ ι h) ∎ where open ≈-Reasoning G.setoid +∙-comm : Commutative Z._≈_ _∙_ +∙-comm g = central g ∘ ι + domain : RawMagma _ _ domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } -ι-isMagmaHomomorphism : IsMagmaHomomorphism domain G.rawMagma ι -ι-isMagmaHomomorphism = record - { isRelHomomorphism = Z.ι-isRelHomomorphism - ; homo = λ _ _ → G.refl +ι-isMagmaMonomorphism : IsMagmaMonomorphism domain G.rawMagma ι +ι-isMagmaMonomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = Z.ι.isHomomorphism + ; homo = λ _ _ → G.refl + } + ; injective = id } +module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism + ------------------------------------------------------------------------ -- Public exports +submagma : Subsemigroup.Submagma _ _ +submagma = record { ι-monomorphism = ι-isMagmaMonomorphism } + semigroup : Semigroup _ _ -semigroup = Subsemigroup.semigroup record - { ι-monomorphism = record - { isMagmaHomomorphism = ι-isMagmaHomomorphism - ; injective = id - } - } +semigroup = Subsemigroup.semigroup submagma commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = record { isSemigroup = isSemigroup - ; comm = λ g → central g ∘ ι + ; comm = ∙-comm } } where open Semigroup semigroup using (isSemigroup) From e5f176e5c747912765b281f66e64ca56cb7c9fc0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 08:43:48 +0000 Subject: [PATCH 22/25] fix: header comments --- src/Algebra/Construct/Centre/Group.agda | 2 +- src/Algebra/Construct/Centre/Monoid.agda | 2 +- src/Algebra/Construct/Centre/Semigroup.agda | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index b0cb99630d..d870bb9797 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Definition of the centre of a Group +-- Definition of Z[ G ] the centre of a Group G ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index 868bc8238f..28441f9b0c 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Definition of the centre of a Group +-- Definition of Z[ G ] the centre of a Monoid G ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 6f1c897cc7..7cf02f5b0d 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Definition of the centre of a Group +-- Definition of Z[ G ] the centre of a Semigroup ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} From dcbdf8e7c83d996a69deb006580ac864590290ab Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 13:08:51 +0000 Subject: [PATCH 23/25] =?UTF-8?q?move:=20`=E2=88=99-comm`=20to=20`Magma`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Construct/Centre/Magma.agda | 3 +++ src/Algebra/Construct/Centre/Semigroup.agda | 5 +---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Construct/Centre/Magma.agda b/src/Algebra/Construct/Centre/Magma.agda index efa1c68502..c87a1dd241 100644 --- a/src/Algebra/Construct/Centre/Magma.agda +++ b/src/Algebra/Construct/Centre/Magma.agda @@ -52,3 +52,6 @@ _≈_ = G._≈_ on ι } module ι = IsRelMonomorphism ι-isRelMonomorphism + +∙-comm : ∀ g h → ι g G.∙ ι h G.≈ ι h G.∙ ι g +∙-comm g h = central g (ι h) diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 7cf02f5b0d..637fef6e4e 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -29,7 +29,7 @@ private -- Definition open Z public - using (Center; ι; central) + using (Center; ι; central; ∙-comm) hiding (module ι) _∙_ : Op₂ Center @@ -43,9 +43,6 @@ central (g ∙ h) = λ k → begin k G.∙ (ι g G.∙ ι h) ∎ where open ≈-Reasoning G.setoid -∙-comm : Commutative Z._≈_ _∙_ -∙-comm g = central g ∘ ι - domain : RawMagma _ _ domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } From d3cac948e693333631734248f159996427f6ce43 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 14:04:56 +0000 Subject: [PATCH 24/25] reconsider: public exports --- src/Algebra/Construct/Centre/Group.agda | 6 ++++-- src/Algebra/Construct/Centre/Monoid.agda | 9 ++++----- src/Algebra/Construct/Centre/Semigroup.agda | 15 +++++++-------- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index d870bb9797..271deb2bbe 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -72,7 +72,9 @@ normalSubgroup = record } open NormalSubgroup normalSubgroup public - hiding (domain; _⁻¹) + using (group) + +module ι = IsGroupMonomorphism ι-isGroupMonomorphism abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ abelianGroup = record @@ -80,7 +82,7 @@ abelianGroup = record { isGroup = isGroup ; comm = ∙-comm } - } + } where open Group group using (isGroup) Z[_] = abelianGroup diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index 28441f9b0c..6139c438dd 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -47,14 +47,14 @@ domain = record { RawMagma Z.domain ; ε = ε } ; injective = id } -module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism +monoid : Monoid _ _ +monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism } ------------------------------------------------------------------------ -- Public exports -monoid : Monoid _ _ -monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism } +module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record @@ -62,8 +62,7 @@ commutativeMonoid = record { isMonoid = isMonoid ; comm = ∙-comm } - } - where open Monoid monoid using (isMonoid) + } where open Monoid monoid using (isMonoid) Z[_] = commutativeMonoid diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index 637fef6e4e..bb3267ad0f 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -55,25 +55,24 @@ domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } ; injective = id } -module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism - - ------------------------------------------------------------------------- --- Public exports - submagma : Subsemigroup.Submagma _ _ submagma = record { ι-monomorphism = ι-isMagmaMonomorphism } semigroup : Semigroup _ _ semigroup = Subsemigroup.semigroup submagma + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism + commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = record { isSemigroup = isSemigroup ; comm = ∙-comm } - } - where open Semigroup semigroup using (isSemigroup) + } where open Semigroup semigroup using (isSemigroup) Z[_] = commutativeSemigroup From e6bd8eaf33ac7eb2d38760b659ff060ab57f6796 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 15:32:55 +0000 Subject: [PATCH 25/25] reconsider: public exports --- src/Algebra/Construct/Centre/Group.agda | 9 ++++----- src/Algebra/Construct/Centre/Magma.agda | 2 +- src/Algebra/Construct/Centre/Monoid.agda | 12 ++++++------ src/Algebra/Construct/Centre/Semigroup.agda | 14 +++++++------- 4 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 271deb2bbe..0dc87797ee 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -14,7 +14,6 @@ import Algebra.Construct.Centre.Monoid as Centre open import Algebra.Core using (Op₁) open import Algebra.Morphism.Structures using (IsGroupMonomorphism) open import Function.Base using (id; _∘_; const; _$_) -open import Level using (_⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup) @@ -62,7 +61,9 @@ domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } ------------------------------------------------------------------------ -- Public exports -normalSubgroup : NormalSubgroup (c ⊔ ℓ) ℓ +module ι = IsGroupMonomorphism ι-isGroupMonomorphism + +normalSubgroup : NormalSubgroup _ _ normalSubgroup = record { subgroup = record { ι-monomorphism = ι-isGroupMonomorphism } ; isNormal = record @@ -74,9 +75,7 @@ normalSubgroup = record open NormalSubgroup normalSubgroup public using (group) -module ι = IsGroupMonomorphism ι-isGroupMonomorphism - -abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ +abelianGroup : AbelianGroup _ _ abelianGroup = record { isAbelianGroup = record { isGroup = isGroup diff --git a/src/Algebra/Construct/Centre/Magma.agda b/src/Algebra/Construct/Centre/Magma.agda index c87a1dd241..23692665e1 100644 --- a/src/Algebra/Construct/Centre/Magma.agda +++ b/src/Algebra/Construct/Centre/Magma.agda @@ -45,7 +45,7 @@ _≈_ = G._≈_ on ι ι-isRelHomomorphism : IsRelHomomorphism _≈_ G._≈_ ι ι-isRelHomomorphism = record { cong = id } -ι-isRelMonomorphism : IsRelMonomorphism _≈_ G._≈_ ι +ι-isRelMonomorphism : IsRelMonomorphism _≈_ _ _ ι-isRelMonomorphism = record { isHomomorphism = ι-isRelHomomorphism ; injective = id diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index 6139c438dd..06bf399dc3 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -50,12 +50,6 @@ domain = record { RawMagma Z.domain ; ε = ε } monoid : Monoid _ _ monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism } - ------------------------------------------------------------------------- --- Public exports - -module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism - commutativeMonoid : CommutativeMonoid _ _ commutativeMonoid = record { isCommutativeMonoid = record @@ -64,5 +58,11 @@ commutativeMonoid = record } } where open Monoid monoid using (isMonoid) + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism + Z[_] = commutativeMonoid diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda index bb3267ad0f..fc86c4483b 100644 --- a/src/Algebra/Construct/Centre/Semigroup.agda +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -46,7 +46,7 @@ central (g ∙ h) = λ k → begin domain : RawMagma _ _ domain = record { _≈_ = Z._≈_; _∙_ = _∙_ } -ι-isMagmaMonomorphism : IsMagmaMonomorphism domain G.rawMagma ι +ι-isMagmaMonomorphism : IsMagmaMonomorphism domain _ _ ι-isMagmaMonomorphism = record { isMagmaHomomorphism = record { isRelHomomorphism = Z.ι.isHomomorphism @@ -61,12 +61,6 @@ submagma = record { ι-monomorphism = ι-isMagmaMonomorphism } semigroup : Semigroup _ _ semigroup = Subsemigroup.semigroup submagma - ------------------------------------------------------------------------- --- Public exports - -module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism - commutativeSemigroup : CommutativeSemigroup _ _ commutativeSemigroup = record { isCommutativeSemigroup = record @@ -75,4 +69,10 @@ commutativeSemigroup = record } } where open Semigroup semigroup using (isSemigroup) + +------------------------------------------------------------------------ +-- Public exports + +module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism + Z[_] = commutativeSemigroup