[ 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,121 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of the centre of a Group
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup; Group)
+
+module Algebra.Construct.Centre.Group {c ℓ} (G : Group c ℓ) where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Definitions using (Commutative)
+open import Function.Base using (id; const; _$_; _on_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Algebra.Construct.Sub.Group G using (Subgroup)
+open import Algebra.Construct.Sub.Group.Normal G using (NormalSubgroup)
+open import Algebra.Properties.Group G using (∙-cancelʳ)
+
+------------------------------------------------------------------------
+-- Definition
+
+private
+  module G = Group G
+
+  open ≈-Reasoning G.setoid
+
+  record Carrier : Set (c ⊔ ℓ) where
+    field
+      commuter : G.Carrier
+      commutes : ∀ k → commuter G.∙ k G.≈ k G.∙ commuter
+
+  open Carrier using (commuter; commutes)
+
+  _≈_ : Rel Carrier ℓ
+  _≈_ = G._≈_ on commuter
+
+  _∙_ : Op₂ Carrier
+  g ∙ h = record
+    { commuter = commuter g G.∙ commuter h
+    ; commutes = λ k → begin
+      (commuter g G.∙ commuter h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩
+      commuter g G.∙ (commuter h G.∙ k) ≈⟨ G.∙-congˡ $ commutes h k ⟩
+      commuter g G.∙ (k G.∙ commuter h) ≈⟨ G.assoc _ _ _ ⟨
+      commuter g G.∙ k G.∙ commuter h   ≈⟨ G.∙-congʳ $ commutes g k ⟩
+      k G.∙ commuter g G.∙ commuter h   ≈⟨ G.assoc _ _ _ ⟩
+      k G.∙ (commuter g G.∙ commuter h) ∎
+    }
+
+  ε : Carrier
+  ε = record
+    { commuter = G.ε
+    ; commutes = λ k → G.trans (G.identityˡ k) (G.sym (G.identityʳ k))
+    }
+
+  _⁻¹ : Op₁ Carrier
+  g ⁻¹ = record
+    { commuter = commuter g G.⁻¹
+    ; commutes = λ k → ∙-cancelʳ (commuter g) _ _ $ begin
+        (commuter g G.⁻¹ G.∙ k) G.∙ (commuter g) ≈⟨ G.assoc _ _ _ ⟩
+        commuter g G.⁻¹ G.∙ (k G.∙ commuter g)   ≈⟨ G.∙-congˡ $ commutes g k ⟨
+        commuter g G.⁻¹ G.∙ (commuter g G.∙ k)   ≈⟨ G.assoc _ _ _ ⟨
+        (commuter g G.⁻¹ G.∙ commuter g) G.∙ k   ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩
+        G.ε G.∙ k                                ≈⟨ commutes ε k ⟩
+        k G.∙ G.ε                                ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨
+        k G.∙ (commuter g G.⁻¹ G.∙ commuter g)   ≈⟨ G.assoc _ _ _ ⟨
+        (k G.∙ commuter g G.⁻¹) G.∙ (commuter g) ∎
+    }
+
+  ∙-comm : Commutative _≈_ _∙_
+  ∙-comm g h = commutes g $ commuter h
+
+  centre : NormalSubgroup (c ⊔ ℓ) ℓ
+  centre = record
+    { subgroup = record
+      { domain = record
+        { _≈_ = _≈_
+        ; _∙_ = _∙_
+        ; ε = ε
+        ; _⁻¹ = _⁻¹
+        }
+      ; ι = commuter
+      ; ι-monomorphism = record
+          { isGroupHomomorphism = record
+            { isMonoidHomomorphism = record
+              { isMagmaHomomorphism = record
+                { isRelHomomorphism = record { cong = id }
+                ; homo = λ _ _ → G.refl
+                }
+              ; ε-homo = G.refl
+              }
+            ; ⁻¹-homo = λ _ → G.refl
+          }
+        ; injective = id
+        }
+      }
+    ; isNormal = record
+      { conjugate = const
+      ; normal = commutes
+      }
+    }
+
+
+------------------------------------------------------------------------
+-- Public exports
+
+open NormalSubgroup centre public
+
+abelianGroup : AbelianGroup (c ⊔ ℓ) ℓ
+abelianGroup = record
+  { isAbelianGroup = record
+    { isGroup = isGroup
+    ; comm = ∙-comm
+    }
+  }
+
+Z[_] = centre

src/Algebra/Construct/Quotient/AbelianGroup.agda

@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient Abelian groups
+------------------------------------------------------------------------
+
+{-# 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?

src/Algebra/Construct/Quotient/Group.agda

@@ -0,0 +1,126 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group)
+open import Algebra.Construct.Sub.Group.Normal using (NormalSubgroup)
+
+module Algebra.Construct.Quotient.Group
+  {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
+
+open import Algebra.Definitions using (Congruent₁; Congruent₂)
+open import Algebra.Morphism.Structures
+  using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Function.Definitions using (Surjective)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+
+private
+  open module G = Group G
+
+open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
+open import Algebra.Properties.Monoid monoid
+open import Relation.Binary.Reasoning.Setoid setoid
+
+private
+  open module N = NormalSubgroup N
+    using (ι; module ι; conjugate; normal)
+
+infix 0 _by_
+
+data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+  _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
+
+≈⇒≋ : _≈_ ⇒ _≋_
+≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _)
+
+≋-refl : Reflexive _≋_
+≋-refl = ≈⇒≋ refl
+
+≋-sym : Symmetric _≋_
+≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
+  ι (g N.⁻¹) ∙ y      ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩
+  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩
+  x                   ∎
+
+≋-trans : Transitive _≋_
+≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
+  ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
+  (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩
+  ι h ∙ y         ≈⟨ ιh∙y≈z ⟩
+  z               ∎
+
+≋-∙-cong : Congruent₂ _≋_ _∙_
+≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
+  ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩
+  (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
+  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
+  y ∙ v                  ∎
+  where h′ = conjugate h x
+
+≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹
+≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
+  ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
+  (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
+  y ⁻¹              ∎
+  where h = conjugate (g N.⁻¹) (x ⁻¹)
+
+quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
+quotientGroup = record
+  { isGroup = record
+    { isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = record
+            { refl = ≋-refl
+            ; sym = ≋-sym
+            ; trans = ≋-trans
+            }
+          ; ∙-cong = ≋-∙-cong
+          }
+        ; assoc = λ x y z → ≈⇒≋ (assoc x y z)
+        }
+      ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ
+      }
+    ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ
+    ; ⁻¹-cong = ≋-⁻¹-cong
+    }
+  }
+
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
+_/_ = quotientGroup
+
+π : Group.Carrier G → Group.Carrier quotientGroup
+π x = x -- because we do all the work in the relation
+
+π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π
+π-isMagmaHomomorphism = record
+  { isRelHomomorphism = record
+    { cong = ≈⇒≋
+    }
+  ; homo = λ _ _ → ≋-refl
+  }
+
+π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π
+π-isMonoidHomomorphism = record
+  { isMagmaHomomorphism = π-isMagmaHomomorphism
+  ; ε-homo = ≋-refl
+  }
+
+π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
+π-isGroupHomomorphism = record
+  { isMonoidHomomorphism = π-isMonoidHomomorphism
+  ; ⁻¹-homo = λ _ → ≋-refl
+  }
+
+π-surjective : Surjective _≈_ _≋_ π
+π-surjective g = g , ≈⇒≋

src/Algebra/Construct/Quotient/Ring.agda

@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup; Ring; RawRing)
+open import Algebra.Construct.Sub.Ring.Ideal using (Ideal)
+
+module Algebra.Construct.Quotient.Ring
+  {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′)
+  where
+
+open import Algebra.Morphism.Structures using (IsRingHomomorphism)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_)
+open import Level using (_⊔_)
+
+import Algebra.Construct.Quotient.AbelianGroup as Quotient
+
+private
+  module R = Ring R
+  module I = Ideal I
+  module R/I = Quotient R.+-abelianGroup I.subgroup
+
+
+open R/I public
+  using (_≋_; _by_; ≋-refl; ≈⇒≋
+        ; quotientAbelianGroup
+        ; π; π-isMonoidHomomorphism; π-surjective
+        )
+
+open import Algebra.Definitions _≋_ using (Congruent₂)
+
+≋-*-cong : Congruent₂ R._*_
+≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
+  ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u       ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩
+  ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u    ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩
+  ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩
+  ι j * ι k + ι j * u + x * ι k + x * u          ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨
+  (ι j + x) * (ι k + u)                          ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩
+  y * v                                          ∎
+  where
+  open R using (_+_; _*_; +-congʳ ;+-cong; *-cong)
+  open import Algebra.Properties.Semiring R.semiring using (binomial-expansion)
+  open import Relation.Binary.Reasoning.Setoid R.setoid
+  open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_)
+
+quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
+quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ }
+
+quotientRing : Ring c (c ⊔ ℓ ⊔ c′)
+quotientRing = record
+  { isRing = record
+    { +-isAbelianGroup = isAbelianGroup
+    ; *-cong = ≋-*-cong
+    ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z)
+    ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ
+    ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z))
+    }
+  } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup)
+
+π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π
+π-isRingHomomorphism = record
+  { isSemiringHomomorphism = record
+    { isNearSemiringHomomorphism = record
+      { +-isMonoidHomomorphism = π-isMonoidHomomorphism
+      ; *-homo = λ _ _ → ≋-refl
+      }
+    ; 1#-homo = ≋-refl
+    }
+  ; -‿homo = λ _ → ≋-refl
+  }
+