[ add ] Algebra.Construct.Centre.X of an algebra X, following #2863

CHANGELOG.md

@@ -84,6 +84,10 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Centre.X` for the definition of the centre of an algebra,
+  where `X = {Semigroup|Monoid|Group|Ring}`, based on an underlying type defined
+  in `Algebra.Construct.Centre.Center`.
+
 * `Algebra.Construct.Sub.Group` for the definition of subgroups.
 
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.

src/Algebra/Construct/Centre/Center.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- 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 (_⊔_)
+import Relation.Binary.Morphism.Construct.On as On
+
+
+------------------------------------------------------------------------
+-- 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
+
+open On _∼_ ι public
+  using (_≈_; isRelHomomorphism; isRelMonomorphism)

src/Algebra/Construct/Centre/Group.agda

@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of the centre of a Group
+------------------------------------------------------------------------
+
+{-# 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
+  using (IsGroupHomomorphism; IsGroupMonomorphism)
+open import Algebra.Morphism.GroupMonomorphism using (isGroup)
+open import Function.Base using (id; const; _$_)
+
+
+private
+  module G = Group group
+
+open import Algebra.Properties.Group group using (∙-cancelʳ)
+open import Algebra.Properties.Monoid G.monoid
+  using (uv≈w⇒xu∙v≈xw)
+  renaming (cancelˡ to inverse⇒cancelˡ; cancelʳ to inverse⇒cancelʳ)
+open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning
+
+
+------------------------------------------------------------------------
+-- 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) ≈⟨ uv≈w⇒xu∙v≈xw (G.sym (Center.central g k)) _ ⟩
+      ι g G.⁻¹ G.∙ (ι g G.∙ k)   ≈⟨ inverse⇒cancelˡ (G.inverseˡ _) _ ⟩
+      k                          ≈⟨ inverse⇒cancelʳ (G.inverseˡ _) _ ⟨
+      (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

src/Algebra/Construct/Centre/Monoid.agda

@@ -0,0 +1,67 @@
+------------------------------------------------------------------------
+-- 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.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
+
+
+------------------------------------------------------------------------
+-- 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 = ε-central
+  }
+
+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

src/Algebra/Construct/Centre/Ring.agda

@@ -0,0 +1,107 @@
+------------------------------------------------------------------------
+-- 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
+  using (IsRingHomomorphism; IsRingMonomorphism)
+open import Algebra.Morphism.RingMonomorphism using (isRing)
+open import Function.Base using (id; const; _$_)
+
+
+private
+  module R = Ring ring
+
+open import Algebra.Properties.Ring ring using (-‿distribˡ-*; -‿distribʳ-*)
+open import Relation.Binary.Reasoning.Setoid R.setoid as ≈-Reasoning
+
+
+------------------------------------------------------------------------
+-- 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

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
+  using (IsMagmaHomomorphism; IsMagmaMonomorphism)
+open import Function.Base using (id; _$_)
+
+private
+  module G = Semigroup semigroup
+
+open import Algebra.Properties.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 ≈⟨ uv≈w⇒xu∙v≈xw (Center.central h k) (ι g) ⟩
+    ι g G.∙ (k G.∙ ι h) ≈⟨ uv≈w⇒u∙vx≈wx (Center.central g k) (ι h) ⟩
+    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
+