[ add ] Algebra.Definitions.Central plus Consequences for Identity and Zero (#2873)

* add: `Algebra.Definitions.Central`

* add: `Identity` and `Zero` elements are `Central`

* Update src/Algebra/Definitions.agda

Co-authored-by: Jacques Carette <[email protected]>

* fix: line break

---------

Co-authored-by: Jacques Carette <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -118,12 +118,21 @@ 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`:
+  ```agda
+  Central : Op₂ A → A → Set _
   ```
 
 * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`:

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
 

src/Algebra/Definitions.agda

@@ -50,6 +50,11 @@ 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)
+
 LeftIdentity : A → Op₂ A → Set _
 LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x