From cbfc19e161e4402fc32ff704bb29ce095e18eda0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 16:54:34 +0000 Subject: [PATCH 1/4] add: `Algebra.Definitions.Central` --- CHANGELOG.md | 5 +++++ src/Algebra/Definitions.agda | 3 +++ 2 files changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3eb803ac39..c3ea84a1cc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -126,6 +126,11 @@ Additions to existing modules ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) ``` +* In `Algebra.Definitions`: + ```agda + Central : Op₂ A → A → Set _ + ``` + * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`: ```agda ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤ diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index e42958da4d..3123ef976d 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -50,6 +50,9 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) Commutative : Op₂ A → Set _ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) +Central : Op₂ A → A → Set _ +Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x) + LeftIdentity : A → Op₂ A → Set _ LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x From 80388380ac948acea844caa6bb81bd6607929fb3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 12 Nov 2025 17:11:02 +0000 Subject: [PATCH 2/4] add: `Identity` and `Zero` elements are `Central` --- CHANGELOG.md | 4 ++++ src/Algebra/Consequences/Setoid.agda | 9 +++++++++ 2 files changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c3ea84a1cc..52fc3d6984 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -118,12 +118,16 @@ Additions to existing modules ```agda binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ → ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + identity⇒central : Identity e _∙_ → Central _∙_ e + zero⇒central : Zero e _∙_ → Central _∙_ e ``` * In `Algebra.Consequences.Setoid`: ```agda binomial-expansion : Congruent₂ _∙_ → Associative _∙_ → _◦_ DistributesOver _∙_ → ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z)) + identity⇒central : Identity e _∙_ → Central _∙_ e + zero⇒central : Zero e _∙_ → Central _∙_ e ``` * In `Algebra.Definitions`: diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 4d6bb4dbba..8ace8652ed 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -184,6 +184,15 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where x ∙ z ≈⟨ comm x z ⟩ z ∙ x ∎ +module _ {_∙_ : Op₂ A} {e : A} where + + identity⇒central : Identity e _∙_ → Central _∙_ e + identity⇒central (identityˡ , identityʳ) x = trans (identityˡ x) (sym (identityʳ x)) + + zero⇒central : Zero e _∙_ → Central _∙_ e + zero⇒central (zeroˡ , zeroʳ) x = trans (zeroˡ x) (sym (zeroʳ x)) + + ------------------------------------------------------------------------ -- Group-like structures From cac627b0d47997b783437192a8b40b0f5355e437 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Tue, 18 Nov 2025 05:26:50 +0000 Subject: [PATCH 3/4] Update src/Algebra/Definitions.agda Co-authored-by: Jacques Carette --- src/Algebra/Definitions.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 3123ef976d..a54c33951d 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -50,6 +50,7 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) Commutative : Op₂ A → Set _ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) +-- An element is called `Central` for a binary operation if it commutes with all other elements. Central : Op₂ A → A → Set _ Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x) From e9dc02f43156fe781228819fdf3a89de286ef2bd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 18 Nov 2025 05:28:56 +0000 Subject: [PATCH 4/4] fix: line break --- src/Algebra/Definitions.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index a54c33951d..d1893e3abd 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -50,7 +50,8 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) Commutative : Op₂ A → Set _ Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x) --- An element is called `Central` for a binary operation if it commutes with all other elements. +-- An element is called `Central` for a binary operation +-- if it commutes with all other elements. Central : Op₂ A → A → Set _ Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x)