[ 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.Centre`.
+
 * `Algebra.Construct.Sub.Group` for the definition of subgroups.
 
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.

src/Algebra/Construct/Centre/Centre.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- 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.Centre
+  {c ℓ} {Carrier : Set c} (_∼_ : Rel Carrier ℓ) (_∙_ : Op₂ Carrier)
+  where
+
+open import Algebra.Definitions _∼_ using (Central)
+open import Level using (_⊔_)
+import Relation.Binary.Morphism.Construct.On as On
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+record Centre : Set (c ⊔ ℓ) where
+  field
+    ι       : Carrier
+    central : Central _∙_ ι
+
+open Centre public
+  using (ι)
+
+∙-comm : ∀ g h → (ι g ∙ ι h) ∼ (ι h ∙ ι g)
+∙-comm g h = Centre.central g (ι h)
+
+-- Centre as subtype of Carrier
+
+open On _∼_ ι public
+  using (_≈_; isRelHomomorphism; isRelMonomorphism)

src/Algebra/Construct/Centre/Group.agda

@@ -0,0 +1,83 @@
+------------------------------------------------------------------------
+-- 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 (IsGroupMonomorphism)
+open import Algebra.Morphism.GroupMonomorphism using (isGroup)
+open import Function.Base using (id; _$_)
+
+
+private
+  module X = Group group
+
+open import Algebra.Properties.Group group using (∙-cancelʳ)
+open import Algebra.Properties.Monoid X.monoid
+  using (uv≈w⇒xu∙v≈xw)
+  renaming (cancelˡ to inverse⇒cancelˡ; cancelʳ to inverse⇒cancelʳ)
+open import Relation.Binary.Reasoning.Setoid X.setoid as ≈-Reasoning
+
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Re-export the underlying sub-Monoid
+
+open import Algebra.Construct.Centre.Monoid X.monoid as Z public
+  using (Centre; ι; ∙-comm)
+
+-- Now, can define a commutative sub-Group
+
+domain : RawGroup _ _
+domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ }
+  where
+  _⁻¹ : Op₁ Centre
+  g ⁻¹ = record
+    { ι = ι g X.⁻¹
+    ; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin
+        (ι g X.⁻¹ X.∙ k) X.∙ (ι g) ≈⟨ uv≈w⇒xu∙v≈xw (X.sym (Centre.central g k)) _ ⟩
+        ι g X.⁻¹ X.∙ (ι g X.∙ k)   ≈⟨ inverse⇒cancelˡ (X.inverseˡ _) _ ⟩
+        k                          ≈⟨ inverse⇒cancelʳ (X.inverseˡ _) _ ⟨
+        (k X.∙ ι g X.⁻¹) X.∙ (ι g) ∎
+    } where open ≈-Reasoning
+
+
+isGroupMonomorphism : IsGroupMonomorphism domain X.rawGroup ι
+isGroupMonomorphism = record
+  { isGroupHomomorphism = record
+    { isMonoidHomomorphism = Z.isMonoidHomomorphism
+    ; ⁻¹-homo = λ _ → X.refl
+    }
+  ; injective = id
+  }
+
+-- Public export of the sub-X-homomorphisms
+
+open IsGroupMonomorphism isGroupMonomorphism public
+
+-- And hence an AbelianGroup
+
+abelianGroup : AbelianGroup _ _
+abelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup isGroupMonomorphism X.isGroup
+    ; comm = ∙-comm
+    }
+  }
+
+-- Public export of the sub-X-structures/bundles
+
+open AbelianGroup abelianGroup public
+
+-- Public export of the bundle
+
+Z[_] = abelianGroup

src/Algebra/Construct/Centre/Monoid.agda

@@ -0,0 +1,74 @@
+------------------------------------------------------------------------
+-- 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 using (IsMonoidMonomorphism)
+open import Algebra.Morphism.MonoidMonomorphism using (isMonoid)
+open import Function.Base using (id)
+
+open import Algebra.Properties.Monoid monoid using (ε-central)
+
+private
+  module X = Monoid monoid
+
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Re-export the underlying sub-Semigroup
+
+open import Algebra.Construct.Centre.Semigroup X.semigroup as Z public
+  using (Centre; ι; ∙-comm)
+
+-- Now, can define a sub-Monoid
+
+domain : RawMonoid _ _
+domain = record { RawMagma Z.domain; ε = ε }
+  where
+  ε : Centre
+  ε = record
+    { ι = X.ε
+    ; central = ε-central
+    }
+
+isMonoidMonomorphism : IsMonoidMonomorphism domain X.rawMonoid ι
+isMonoidMonomorphism = record
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = Z.isMagmaHomomorphism
+    ; ε-homo = X.refl
+    }
+  ; injective = id
+  }
+
+-- Public export of the sub-X-homomorphisms
+
+open IsMonoidMonomorphism isMonoidMonomorphism public
+
+-- And hence a CommutativeMonoid
+
+commutativeMonoid : CommutativeMonoid _ _
+commutativeMonoid = record
+  { isCommutativeMonoid = record
+    { isMonoid = isMonoid isMonoidMonomorphism X.isMonoid
+    ; comm = ∙-comm
+    }
+  }
+
+-- Public export of the sub-X-structures/bundles
+
+open CommutativeMonoid commutativeMonoid public
+
+-- Public export of the bundle
+
+Z[_] = commutativeMonoid

src/Algebra/Construct/Centre/Ring.agda

@@ -0,0 +1,114 @@
+------------------------------------------------------------------------
+-- 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 (IsRingMonomorphism)
+open import Algebra.Morphism.RingMonomorphism using (isRing)
+open import Function.Base using (id)
+
+
+private
+  module X = Ring ring
+
+open import Algebra.Properties.Ring ring using (-‿distribˡ-*; -‿distribʳ-*)
+open import Relation.Binary.Reasoning.Setoid X.setoid as ≈-Reasoning
+
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Re-export the underlying sub-Monoid
+
+open import Algebra.Construct.Centre.Monoid X.*-monoid as Z public
+  using (Centre; ι; ∙-comm)
+
+-- Now, can define a commutative sub-Ring
+
+domain : RawRing _ _
+domain = record
+  { _≈_ = _≈_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; -_ = -_
+  ; 0# = 0#
+  ; 1# = 1#
+  }
+  where
+  open RawMonoid Z.domain renaming (ε to 1#; _∙_ to _*_)
+  _+_ : Op₂ Centre
+  g + h = record
+    { ι       = ι g X.+ ι h
+    ; central = λ r → begin
+      (ι g X.+ ι h) X.* r      ≈⟨ X.distribʳ _ _ _ ⟩
+      ι g X.* r X.+ ι h X.* r  ≈⟨ X.+-cong (Centre.central g r) (Centre.central h r) ⟩
+      r X.* ι g  X.+ r X.* ι h ≈⟨ X.distribˡ _ _ _ ⟨
+      r X.* (ι g X.+ ι h)      ∎
+    }
+  -_ : Op₁ Centre
+  - g = record
+    { ι       = X.- ι g
+    ; central = λ r → begin
+      X.- ι g X.* r   ≈⟨ -‿distribˡ-* (ι g) r ⟨
+      X.- (ι g X.* r) ≈⟨ X.-‿cong (Centre.central g r) ⟩
+      X.- (r X.* ι g) ≈⟨ -‿distribʳ-* r (ι g) ⟩
+      r  X.* X.- ι g  ∎
+    }
+  0# : Centre
+  0# = record
+    { ι = X.0#
+    ; central = zero⇒central X.setoid {_∙_ = X._*_} X.zero
+    }
+
+isRingMonomorphism : IsRingMonomorphism domain X.rawRing ι
+isRingMonomorphism = record
+  { isRingHomomorphism = record
+    { isSemiringHomomorphism = record
+      { isNearSemiringHomomorphism = record
+        { +-isMonoidHomomorphism = record
+          { isMagmaHomomorphism = record
+            { isRelHomomorphism = record { cong = id }
+            ; homo = λ _ _ → X.refl
+            }
+          ; ε-homo = X.refl
+          }
+        ; *-homo = λ _ _ → X.refl
+        }
+      ; 1#-homo = X.refl
+      }
+    ; -‿homo = λ _ → X.refl
+    }
+    ; injective = id
+  }
+
+-- Public export of the sub-X-homomorphisms
+
+open IsRingMonomorphism isRingMonomorphism public
+
+-- And hence a CommutativeRing
+
+commutativeRing : CommutativeRing _ _
+commutativeRing = record
+  { isCommutativeRing = record
+    { isRing = isRing isRingMonomorphism X.isRing
+    ; *-comm = ∙-comm
+    }
+  }
+
+-- Public export of the sub-X-structures/bundles
+
+open CommutativeRing commutativeRing public
+
+-- Public export of the bundle
+
+Z[_] = commutativeRing