refactor: alternative to agda#2852 and agda#2854

Author: jamesmckinna

CHANGELOG.md

@@ -79,6 +79,12 @@ Deprecated names
 New modules
 -----------
 
+* `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.Properties.BooleanRing`.
 
 * `Algebra.Properties.BooleanSemiring`.

src/Algebra/Construct/Sub/AbelianGroup.agda

@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Subgroups of Abelian groups: necessarily Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (AbelianGroup)
+
+module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where
+
+open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup)
+
+private
+  module G = AbelianGroup G
+
+open import Algebra.Construct.Sub.Group.Normal G.group
+  using (IsNormal; NormalSubgroup)
+
+-- Re-export the notion of subgroup of the underlying Group
+
+open import Algebra.Construct.Sub.Group G.group public
+  using (Subgroup)
+
+-- Then, for any such Subgroup:
+-- * it defines an AbelianGroup
+-- * and is, in fact, Normal
+
+module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where
+
+  open Subgroup subgroup public
+    using (ι; ι-monomorphism)
+
+  abelianGroup : AbelianGroup c′ ℓ′
+  abelianGroup = record
+    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
+
+  open AbelianGroup abelianGroup public
+
+  isNormal : IsNormal subgroup
+  isNormal = record { normal = λ n → G.comm (ι n) }
+
+  normalSubgroup : NormalSubgroup c′ ℓ′
+  normalSubgroup = record { isNormal = isNormal }
+
+  open NormalSubgroup normalSubgroup public
+    using (conjugate; normal)

src/Algebra/Construct/Sub/Group.agda

@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of subgroup via Group monomorphism
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group; RawGroup)
+
+module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where
+
+open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
+open import Algebra.Morphism.GroupMonomorphism using (isGroup)
+open import Level using (suc; _⊔_)
+
+private
+  module G = Group G
+
+record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    domain         : RawGroup c′ ℓ′
+    ι              : _ → G.Carrier
+    ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
+
+  module ι = IsGroupMonomorphism ι-monomorphism
+
+  group : Group _ _
+  group = record { isGroup = isGroup ι-monomorphism G.isGroup }
+
+  open Group group public

src/Algebra/Construct/Sub/Group/Normal.agda

@@ -0,0 +1,32 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of normal subgroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group)
+
+module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ)  where
+
+open import Algebra.Construct.Sub.Group G using (Subgroup)
+open import Level using (suc; _⊔_)
+
+private
+  module G = Group G
+
+-- every element of the subgroup commutes in G
+record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
+  open Subgroup subgroup using (ι)
+  field
+    conjugate : ∀ n g → _
+    normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
+
+record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    subgroup : Subgroup c′ ℓ′
+    isNormal : IsNormal subgroup
+
+  open Subgroup subgroup public
+  open IsNormal isNormal public