[ add ] Centre of a Group etc.

CHANGELOG.md

@@ -79,6 +79,18 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Construct.Centre.Group` for the definition of the centre of a group.
+
+* `Algebra.Construct.Quotient.{Abelian}Group` for the definition of quotient (Abelian) groups.
+
+* `Algebra.Construct.Sub.{Abelian}Group` for the definition of sub-(Abelian)groups.
+
+* `Algebra.Construct.Sub.Group.Normal` for the definition of normal subgroups.
+
+* `Algebra.Construct.Sub.Ring.Ideal` for the definition of ideals of a ring.
+
+* `Algebra.Module.Construct.Sub.Bimodule` for the definition of sub-bimodules.
+
 * `Algebra.Properties.BooleanRing`.
 
 * `Algebra.Properties.BooleanSemiring`.

src/Algebra/Construct/Centre/Group.agda

@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of Z[ G ] the centre of a Group G
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup; Group; RawGroup; RawMonoid)
+
+module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where
+
+import Algebra.Construct.Centre.Monoid as Centre
+open import Algebra.Core using (Op₁)
+open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
+open import Function.Base using (id; _∘_; const; _$_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup)
+open import Algebra.Properties.Group G using (∙-cancelʳ)
+
+private
+  module G = Group G
+  module Z = Centre G.monoid
+
+
+------------------------------------------------------------------------
+-- Definition
+
+open Z public
+  using (Center; ι; central; ∙-comm)
+  hiding (module ι)
+
+_⁻¹ : 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ˡ $ central g k ⟨
+      ι g G.⁻¹ G.∙ (ι g G.∙ k)   ≈⟨ G.assoc _ _ _ ⟨
+      (ι g G.⁻¹ G.∙ ι g) G.∙ k   ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩
+      G.ε G.∙ k                  ≈⟨ 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 G.setoid
+
+domain : RawGroup _ _
+domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ }
+
+ι-isGroupMonomorphism : IsGroupMonomorphism domain _ _
+ι-isGroupMonomorphism = record
+  { isGroupHomomorphism = record
+    { isMonoidHomomorphism = Z.ι.isMonoidHomomorphism
+    ; ⁻¹-homo = λ _ → G.refl
+    }
+  ; injective = id
+  }
+
+
+------------------------------------------------------------------------
+-- Public exports
+
+module ι = IsGroupMonomorphism ι-isGroupMonomorphism
+
+normalSubgroup : NormalSubgroup _ _
+normalSubgroup = record
+  { subgroup = record { ι-monomorphism = ι-isGroupMonomorphism }
+  ; isNormal = record
+    { conjugate = const
+    ; normal = central
+    }
+  }
+
+open NormalSubgroup normalSubgroup public
+  using (group)
+
+abelianGroup : AbelianGroup _ _
+abelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup
+    ; comm = ∙-comm
+    }
+  } where open Group group using (isGroup)
+
+Z[_] = abelianGroup
+

src/Algebra/Construct/Centre/Magma.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of the centre of a Magma
+--
+-- NB this doesn't make sense a priori, because in the absence of
+-- associativity, it's not possible to define even a Magma operation
+-- on the Center type defined below, as underlying Carrier.
+--
+-- Yet a Magma *is* sufficient to define such a type, and thus can be
+-- inherited up through the whole `Algebra.Construct.Centre.X` hierarchy.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Magma)
+
+module Algebra.Construct.Centre.Magma {c ℓ} (G : Magma c ℓ) where
+
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Central)
+open import Function.Base using (id; _on_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+private
+  module G = Magma G
+
+
+------------------------------------------------------------------------
+-- Definition
+
+record Center : Set (c ⊔ ℓ) where
+  field
+    ι       : G.Carrier
+    central : Central G._≈_ G._∙_ ι
+
+open Center public
+
+_≈_ : Rel Center _
+_≈_ = G._≈_ on ι
+
+ι-isRelHomomorphism : IsRelHomomorphism _≈_ G._≈_ ι
+ι-isRelHomomorphism = record { cong = id }
+
+ι-isRelMonomorphism : IsRelMonomorphism _≈_ _ _
+ι-isRelMonomorphism = record
+  { isHomomorphism = ι-isRelHomomorphism
+  ; injective = id
+  }
+
+module ι = IsRelMonomorphism ι-isRelMonomorphism
+
+∙-comm : ∀ g h → ι g G.∙ ι h G.≈ ι h G.∙ ι g 
+∙-comm g h = central g (ι h)

src/Algebra/Construct/Centre/Monoid.agda

@@ -0,0 +1,68 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of Z[ G ] the centre of a Monoid G
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles
+  using (CommutativeMonoid; Monoid; RawMonoid; RawMagma)
+
+module Algebra.Construct.Centre.Monoid {c ℓ} (G : Monoid c ℓ) where
+
+open import Algebra.Morphism.Structures using (IsMonoidMonomorphism)
+open import Function.Base using (id; _∘_)
+
+import Algebra.Construct.Centre.Semigroup as Centre
+open import Algebra.Construct.Sub.Monoid G using (Submonoid)
+
+private
+  module G = Monoid G
+  module Z = Centre G.semigroup
+
+
+------------------------------------------------------------------------
+-- Definition
+
+open Z public
+  using (Center; ι; central; ∙-comm)
+  hiding (module ι)
+
+ε : Center
+ε = record
+  { ι = G.ε
+  ; central = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k))
+  }
+
+domain : RawMonoid _ _
+domain = record { RawMagma Z.domain ; ε = ε }
+
+ι-isMonoidMonomorphism : IsMonoidMonomorphism domain _ _
+ι-isMonoidMonomorphism = record
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = Z.ι.isMagmaHomomorphism
+    ; ε-homo = G.refl
+    }
+  ; injective = id
+  }
+
+monoid : Monoid _ _
+monoid = Submonoid.monoid record { ι-monomorphism = ι-isMonoidMonomorphism }
+
+commutativeMonoid : CommutativeMonoid _ _
+commutativeMonoid = record
+  { isCommutativeMonoid = record
+    { isMonoid = isMonoid
+    ; comm = ∙-comm
+    }
+  } where open Monoid monoid using (isMonoid)
+
+
+------------------------------------------------------------------------
+-- Public exports
+
+module ι = IsMonoidMonomorphism ι-isMonoidMonomorphism
+
+Z[_] = commutativeMonoid
+

src/Algebra/Construct/Centre/Semigroup.agda

@@ -0,0 +1,78 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of Z[ G ] the centre of a Semigroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (CommutativeSemigroup; Semigroup; RawMagma)
+
+module Algebra.Construct.Centre.Semigroup {c ℓ} (G : Semigroup c ℓ) where
+
+import Algebra.Construct.Centre.Magma as Centre
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Commutative)
+open import Algebra.Morphism.Structures using (IsMagmaMonomorphism)
+open import Function.Base using (id; _∘_; const; _$_; _on_)
+open import Level using (_⊔_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+import Algebra.Construct.Sub.Semigroup G as Subsemigroup
+
+private
+  module G = Semigroup G
+  module Z = Centre G.magma
+
+
+------------------------------------------------------------------------
+-- Definition
+
+open Z public
+  using (Center; ι; central; ∙-comm)
+  hiding (module ι)
+
+_∙_ : Op₂ Center
+ι       (g ∙ h) = ι g G.∙ ι h
+central (g ∙ h) = λ k → begin
+  (ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩
+  ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ central h k ⟩
+  ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨
+  ι g G.∙ k G.∙ ι h   ≈⟨ G.∙-congʳ $ central g k ⟩
+  k G.∙ ι g G.∙ ι h   ≈⟨ G.assoc _ _ _ ⟩
+  k G.∙ (ι g G.∙ ι h) ∎
+  where open ≈-Reasoning G.setoid
+
+domain : RawMagma _ _
+domain = record { _≈_ = Z._≈_; _∙_ = _∙_ }
+
+ι-isMagmaMonomorphism : IsMagmaMonomorphism domain _ _
+ι-isMagmaMonomorphism = record
+  { isMagmaHomomorphism = record
+    { isRelHomomorphism = Z.ι.isHomomorphism
+    ; homo = λ _ _ → G.refl
+    }
+  ; injective = id
+  }
+
+submagma : Subsemigroup.Submagma _ _
+submagma = record { ι-monomorphism = ι-isMagmaMonomorphism }
+
+semigroup : Semigroup _ _
+semigroup = Subsemigroup.semigroup submagma
+
+commutativeSemigroup : CommutativeSemigroup _ _
+commutativeSemigroup = record
+  { isCommutativeSemigroup = record
+    { isSemigroup = isSemigroup
+    ; comm = ∙-comm
+    }
+  } where open Semigroup semigroup using (isSemigroup)
+
+
+------------------------------------------------------------------------
+-- Public exports
+
+module ι = IsMagmaMonomorphism ι-isMagmaMonomorphism
+
+Z[_] = commutativeSemigroup

src/Algebra/Construct/Quotient/AbelianGroup.agda

@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient of an Abelian group by a subgroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group; AbelianGroup)
+import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
+
+module Algebra.Construct.Quotient.AbelianGroup
+  {c ℓ} (G : AbelianGroup c ℓ)
+  (open AbelianSubgroup G using (Subgroup; normalSubgroup))
+  {c′ ℓ′} (N : Subgroup c′ ℓ′)
+  where
+
+private
+  module G = AbelianGroup G
+
+-- Re-export the quotient group
+
+open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public
+
+-- With its additional bundle
+
+quotientAbelianGroup : AbelianGroup c _
+quotientAbelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup
+    ; comm = λ g h → ≈⇒≋ (G.comm g h)
+    }
+  } where open Group quotientGroup
+
+-- Public re-exports, as needed?