add: Centre of an algebra, following agda#2863

Author: jamesmckinna

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.

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
+  }

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
+      }
+    }
+-}

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

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
+