From 46d8280f1ac2dbc399b42d6a6becc1b31c543e5d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 19 Nov 2025 13:26:47 +0000 Subject: [PATCH 1/7] add: `Centre` of an algebra, following #2863 --- CHANGELOG.md | 4 + src/Algebra/Construct/Centre/Center.agda | 49 ++++++++++++ src/Algebra/Construct/Centre/Group.agda | 85 +++++++++++++++++++++ src/Algebra/Construct/Centre/Monoid.agda | 66 ++++++++++++++++ src/Algebra/Construct/Centre/Semigroup.agda | 75 ++++++++++++++++++ 5 files changed, 279 insertions(+) create mode 100644 src/Algebra/Construct/Centre/Center.agda create mode 100644 src/Algebra/Construct/Centre/Group.agda create mode 100644 src/Algebra/Construct/Centre/Monoid.agda create mode 100644 src/Algebra/Construct/Centre/Semigroup.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 52fc3d6984..d30827c5b7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -79,6 +79,10 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Centre.X` for the definition of the centre of an algebra, + where `X = {Semigroup|Monoid|Group}`, based on an underlying type defined in + `Algebra.Construct.Centre`. + * `Algebra.Construct.Sub.Group` for the definition of subgroups. * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules. diff --git a/src/Algebra/Construct/Centre/Center.agda b/src/Algebra/Construct/Centre/Center.agda new file mode 100644 index 0000000000..cb8cfb3252 --- /dev/null +++ b/src/Algebra/Construct/Centre/Center.agda @@ -0,0 +1,49 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre as a subtype of (the carrier of) a raw magma +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Core using (Op₂) +open import Relation.Binary.Core using (Rel) + +module Algebra.Construct.Centre.Center + {c ℓ} {Carrier : Set c} (_∼_ : Rel Carrier ℓ) (_∙_ : Op₂ Carrier) + where + +open import Algebra.Definitions _∼_ using (Central) +open import Function.Base using (id; _on_) +open import Level using (_⊔_) +open import Relation.Binary.Morphism.Structures + using (IsRelHomomorphism; IsRelMonomorphism) + + +------------------------------------------------------------------------ +-- Definitions + +record Center : Set (c ⊔ ℓ) where + field + ι : Carrier + central : Central _∙_ ι + +open Center public + using (ι) + +∙-comm : ∀ g h → (ι g ∙ ι h) ∼ (ι h ∙ ι g) +∙-comm g h = Center.central g (ι h) + +-- Center as subtype of Carrier + +_≈_ : Rel Center _ +_≈_ = _∼_ on ι + +isRelHomomorphism : IsRelHomomorphism _≈_ _∼_ ι +isRelHomomorphism = record { cong = id } + +isRelMonomorphism : IsRelMonomorphism _≈_ _∼_ ι +isRelMonomorphism = record + { isHomomorphism = isRelHomomorphism + ; injective = id + } diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda new file mode 100644 index 0000000000..745d2434bd --- /dev/null +++ b/src/Algebra/Construct/Centre/Group.agda @@ -0,0 +1,85 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of an Algebra +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (Group; AbelianGroup; RawMonoid; RawGroup) + +module Algebra.Construct.Centre.Group {c ℓ} (group : Group c ℓ) where + +open import Algebra.Core using (Op₁) +open import Algebra.Morphism.Structures +open import Algebra.Morphism.GroupMonomorphism using (isGroup) +open import Function.Base using (id; const; _$_) + + +private + module G = Group group + +open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning +open import Algebra.Properties.Group group using (∙-cancelʳ) + + +------------------------------------------------------------------------ +-- Definition + +-- Re-export the underlying sub-Monoid + +open import Algebra.Construct.Centre.Monoid G.monoid as Z public + using (Center; ι; ∙-comm) + +-- Now, can define a commutative sub-Group + +_⁻¹ : 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ˡ $ Center.central g k ⟨ + ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ + (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ + G.ε G.∙ k ≈⟨ Center.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 + +domain : RawGroup _ _ +domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ } + +isGroupHomomorphism : IsGroupHomomorphism domain G.rawGroup ι +isGroupHomomorphism = record + { isMonoidHomomorphism = Z.isMonoidHomomorphism + ; ⁻¹-homo = λ _ → G.refl + } + +isGroupMonomorphism : IsGroupMonomorphism domain G.rawGroup ι +isGroupMonomorphism = record + { isGroupHomomorphism = isGroupHomomorphism + ; injective = id + } + +abelianGroup : AbelianGroup _ _ +abelianGroup = record + { isAbelianGroup = record + { isGroup = isGroup isGroupMonomorphism G.isGroup + ; comm = ∙-comm + } + } + +Z[_] = abelianGroup + +{- + normalSubgroup : NormalSubgroup _ _ + normalSubgroup = record + { subgroup = record { ι-isGroupMonomorphism = isGroupMonomorphism } + ; normal = record + { conjugate = const + ; normal = Center.central + } + } +-} diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda new file mode 100644 index 0000000000..d08dae966e --- /dev/null +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -0,0 +1,66 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of an Monoid +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (Monoid; CommutativeMonoid; RawMagma; RawMonoid) + +module Algebra.Construct.Centre.Monoid + {c ℓ} (monoid : Monoid c ℓ) + where + +open import Algebra.Consequences.Setoid using (identity⇒central) +open import Algebra.Morphism.Structures +open import Algebra.Morphism.MonoidMonomorphism using (isMonoid) +open import Function.Base using (id) + +private + module G = Monoid monoid + + +------------------------------------------------------------------------ +-- Definition + +-- Re-export the underlying sub-Semigroup + +open import Algebra.Construct.Centre.Semigroup G.semigroup as Z public + using (Center; ι; ∙-comm) + +-- Now, can define a sub-Monoid + +ε : Center +ε = record + { ι = G.ε + ; central = identity⇒central G.setoid {_∙_ = G._∙_} G.identity + } + +domain : RawMonoid _ _ +domain = record { RawMagma Z.domain; ε = ε } + +isMonoidHomomorphism : IsMonoidHomomorphism domain G.rawMonoid ι +isMonoidHomomorphism = record + { isMagmaHomomorphism = Z.isMagmaHomomorphism + ; ε-homo = G.refl + } + +isMonoidMonomorphism : IsMonoidMonomorphism domain G.rawMonoid ι +isMonoidMonomorphism = record + { isMonoidHomomorphism = isMonoidHomomorphism + ; injective = id + } + +-- And hence a CommutativeMonoid + +commutativeMonoid : CommutativeMonoid _ _ +commutativeMonoid = record + { isCommutativeMonoid = record + { isMonoid = isMonoid isMonoidMonomorphism G.isMonoid + ; comm = ∙-comm + } + } + +Z[_] = commutativeMonoid diff --git a/src/Algebra/Construct/Centre/Semigroup.agda b/src/Algebra/Construct/Centre/Semigroup.agda new file mode 100644 index 0000000000..74ca73122f --- /dev/null +++ b/src/Algebra/Construct/Centre/Semigroup.agda @@ -0,0 +1,75 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of an Semigroup +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (Semigroup; CommutativeSemigroup; RawMagma) + +module Algebra.Construct.Centre.Semigroup + {c ℓ} (semigroup : Semigroup c ℓ) + where + +open import Algebra.Core using (Op₂) +open import Algebra.Morphism.MagmaMonomorphism using (isSemigroup) +open import Algebra.Morphism.Structures +open import Function.Base using (id; _$_) + +private + module G = Semigroup semigroup + +open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning + + +------------------------------------------------------------------------ +-- Definition + +-- Re-export the underlying subtype + +open import Algebra.Construct.Centre.Center G._≈_ G._∙_ as Z public + using (Center; ι; ∙-comm) + +-- Now, by associativity, a sub-Magma is definable + +_∙_ : 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ˡ $ Center.central h k ⟩ + ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ Center.central g k ⟩ + k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩ + k G.∙ (ι g G.∙ ι h) ∎ + } where open ≈-Reasoning + +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 = isMagmaHomomorphism + ; injective = id + } + +-- And hence a CommutativeSemigroup + +commutativeSemigroup : CommutativeSemigroup _ _ +commutativeSemigroup = record + { isCommutativeSemigroup = record + { isSemigroup = isSemigroup isMagmaMonomorphism G.isSemigroup + ; comm = ∙-comm + } + } + +Z[_] = commutativeSemigroup + From c94d9b544d5980df0e62f5ece5681a8e61a3310b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 19 Nov 2025 13:40:48 +0000 Subject: [PATCH 2/7] fix: typo --- src/Algebra/Construct/Centre/Group.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 745d2434bd..876ad414f3 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 an Algebra +-- Definition of the centre of a Group ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-} From 00db5c22cd9c4989f10817675a53ef6e2a5dd78b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 19 Nov 2025 18:05:39 +0000 Subject: [PATCH 3/7] add: centre of a `Ring` --- CHANGELOG.md | 4 +- src/Algebra/Construct/Centre/Ring.agda | 106 +++++++++++++++++++++++++ 2 files changed, 108 insertions(+), 2 deletions(-) create mode 100644 src/Algebra/Construct/Centre/Ring.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index d30827c5b7..0ca1d2322f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -80,8 +80,8 @@ New modules ----------- * `Algebra.Construct.Centre.X` for the definition of the centre of an algebra, - where `X = {Semigroup|Monoid|Group}`, based on an underlying type defined in - `Algebra.Construct.Centre`. + where `X = {Semigroup|Monoid|Group|Ring}`, based on an underlying type defined + in `Algebra.Construct.Centre`. * `Algebra.Construct.Sub.Group` for the definition of subgroups. diff --git a/src/Algebra/Construct/Centre/Ring.agda b/src/Algebra/Construct/Centre/Ring.agda new file mode 100644 index 0000000000..c5b4da52ee --- /dev/null +++ b/src/Algebra/Construct/Centre/Ring.agda @@ -0,0 +1,106 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definition of the centre of a Ring +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Bundles + using (Ring; CommutativeRing; Monoid; RawRing; RawMonoid) + +module Algebra.Construct.Centre.Ring {c ℓ} (ring : Ring c ℓ) where + +open import Algebra.Core using (Op₁; Op₂) +open import Algebra.Consequences.Setoid using (zero⇒central) +open import Algebra.Morphism.Structures +open import Algebra.Morphism.RingMonomorphism using (isRing) +open import Function.Base using (id; const; _$_) + + +private + module R = Ring ring + module R* = Monoid R.*-monoid + +open import Relation.Binary.Reasoning.Setoid R.setoid as ≈-Reasoning +open import Algebra.Properties.Ring ring using (-‿distribˡ-*; -‿distribʳ-*) + + +------------------------------------------------------------------------ +-- Definition + +-- Re-export the underlying sub-Monoid + +open import Algebra.Construct.Centre.Monoid R.*-monoid as Z public + using (Center; ι; ∙-comm) + +-- Now, can define a commutative sub-Ring + +_+_ : Op₂ Center +g + h = record + { ι = ι g R.+ ι h + ; central = λ r → begin + (ι g R.+ ι h) R.* r ≈⟨ R.distribʳ _ _ _ ⟩ + ι g R.* r R.+ ι h R.* r ≈⟨ R.+-cong (Center.central g r) (Center.central h r) ⟩ + r R.* ι g R.+ r R.* ι h ≈⟨ R.distribˡ _ _ _ ⟨ + r R.* (ι g R.+ ι h) ∎ + } + +-_ : Op₁ Center +- g = record + { ι = R.- ι g + ; central = λ r → begin R.- ι g R.* r ≈⟨ -‿distribˡ-* (ι g) r ⟨ + R.- (ι g R.* r) ≈⟨ R.-‿cong (Center.central g r) ⟩ + R.- (r R.* ι g) ≈⟨ -‿distribʳ-* r (ι g) ⟩ + r R.* R.- ι g ∎ + } + +0# : Center +0# = record + { ι = R.0# + ; central = zero⇒central R.setoid {_∙_ = R._*_} R.zero + } + +domain : RawRing _ _ +domain = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } where open RawMonoid Z.domain renaming (ε to 1#; _∙_ to _*_) + +isRingHomomorphism : IsRingHomomorphism domain R.rawRing ι +isRingHomomorphism = record + { isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = id } + ; homo = λ _ _ → R.refl + } + ; ε-homo = R.refl + } + ; *-homo = λ _ _ → R.refl + } + ; 1#-homo = R.refl + } + ; -‿homo = λ _ → R.refl + } + +isRingMonomorphism : IsRingMonomorphism domain R.rawRing ι +isRingMonomorphism = record + { isRingHomomorphism = isRingHomomorphism + ; injective = id + } + +commutativeRing : CommutativeRing _ _ +commutativeRing = record + { isCommutativeRing = record + { isRing = isRing isRingMonomorphism R.isRing + ; *-comm = ∙-comm + } + } + +Z[_] = commutativeRing From 210d9db224c83ead991bde6f9cb3eb14edca83ae Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 21 Nov 2025 05:40:59 +0000 Subject: [PATCH 4/7] fix: remove commented-out code --- src/Algebra/Construct/Centre/Group.agda | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 876ad414f3..02be0f040e 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -72,14 +72,3 @@ abelianGroup = record } Z[_] = abelianGroup - -{- - normalSubgroup : NormalSubgroup _ _ - normalSubgroup = record - { subgroup = record { ι-isGroupMonomorphism = isGroupMonomorphism } - ; normal = record - { conjugate = const - ; normal = Center.central - } - } --} From d0ea58e34371fb9f14b57fa7abfa992c32442111 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 21 Nov 2025 06:26:02 +0000 Subject: [PATCH 5/7] refactor: use `Monoid` reasoning principles --- src/Algebra/Construct/Centre/Group.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Construct/Centre/Group.agda b/src/Algebra/Construct/Centre/Group.agda index 02be0f040e..55600c6c90 100644 --- a/src/Algebra/Construct/Centre/Group.agda +++ b/src/Algebra/Construct/Centre/Group.agda @@ -21,6 +21,8 @@ private module G = Group group open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning +open import Algebra.Properties.Monoid G.monoid + renaming (cancelˡ to inverse⇒cancelˡ; cancelʳ to inverse⇒cancelʳ) open import Algebra.Properties.Group group using (∙-cancelʳ) @@ -40,11 +42,8 @@ g ⁻¹ = record ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin (ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩ ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ Center.central g k ⟨ - ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨ - (ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩ - G.ε G.∙ k ≈⟨ Center.central Z.ε k ⟩ - k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨ - k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨ + ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ inverse⇒cancelˡ (G.inverseˡ _) _ ⟩ + k ≈⟨ inverse⇒cancelʳ (G.inverseˡ _) _ ⟨ (k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎ } where open ≈-Reasoning From 172bdc8e4b7c396a2ab823af6d5c69c7ed1367a2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 21 Nov 2025 08:29:08 +0000 Subject: [PATCH 6/7] =?UTF-8?q?refactor:=20use=20`=CE=B5-central`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Construct/Centre/Monoid.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Construct/Centre/Monoid.agda b/src/Algebra/Construct/Centre/Monoid.agda index d08dae966e..aa09870096 100644 --- a/src/Algebra/Construct/Centre/Monoid.agda +++ b/src/Algebra/Construct/Centre/Monoid.agda @@ -13,11 +13,12 @@ module Algebra.Construct.Centre.Monoid {c ℓ} (monoid : Monoid c ℓ) where -open import Algebra.Consequences.Setoid using (identity⇒central) open import Algebra.Morphism.Structures open import Algebra.Morphism.MonoidMonomorphism using (isMonoid) open import Function.Base using (id) +open import Algebra.Properties.Monoid monoid using (ε-central) + private module G = Monoid monoid @@ -35,7 +36,7 @@ open import Algebra.Construct.Centre.Semigroup G.semigroup as Z public ε : Center ε = record { ι = G.ε - ; central = identity⇒central G.setoid {_∙_ = G._∙_} G.identity + ; central = ε-central } domain : RawMonoid _ _ From 703121cd07b95672cc9e95fa43e0cb8291fe4b32 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 21 Nov 2025 08:33:02 +0000 Subject: [PATCH 7/7] refactor: use `Relation.Binary.Morphism.Construct.On` --- src/Algebra/Construct/Centre/Center.agda | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Construct/Centre/Center.agda b/src/Algebra/Construct/Centre/Center.agda index cb8cfb3252..0d767f25a9 100644 --- a/src/Algebra/Construct/Centre/Center.agda +++ b/src/Algebra/Construct/Centre/Center.agda @@ -16,8 +16,7 @@ module Algebra.Construct.Centre.Center open import Algebra.Definitions _∼_ using (Central) open import Function.Base using (id; _on_) open import Level using (_⊔_) -open import Relation.Binary.Morphism.Structures - using (IsRelHomomorphism; IsRelMonomorphism) +import Relation.Binary.Morphism.Construct.On as On ------------------------------------------------------------------------ @@ -36,14 +35,5 @@ open Center public -- Center as subtype of Carrier -_≈_ : Rel Center _ -_≈_ = _∼_ on ι - -isRelHomomorphism : IsRelHomomorphism _≈_ _∼_ ι -isRelHomomorphism = record { cong = id } - -isRelMonomorphism : IsRelMonomorphism _≈_ _∼_ ι -isRelMonomorphism = record - { isHomomorphism = isRelHomomorphism - ; injective = id - } +open On _∼_ ι public + using (_≈_; isRelHomomorphism; isRelMonomorphism)