comment: extensively on AbelianSubgroup

Author: jamesmckinna

src/Algebra/Construct/Sub/AbelianGroup.agda

@@ -2,6 +2,12 @@
 -- The Agda standard library
 --
 -- Subgroups of Abelian groups: necessarily Normal
+--
+-- This is a strict addition/extension to Nathan van Doorn (Taneb)'s PR
+-- https://github.com/agda/agda-stdlib/pull/2852
+-- and avoids the lemma `Algebra.NormalSubgroup.abelian⇒subgroup-normal`
+-- introduced in PR https://github.com/agda/agda-stdlib/pull/2854
+-- in favour of the direct definition of the field `normal` below.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
@@ -10,11 +16,21 @@ open import Algebra.Bundles using (AbelianGroup)
 
 module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where
 
+-- As with the corresponding appeal to `IsGroup` in the module
+-- `Algebra.Construct.Sub.AbelianGroup`, this import drives the export
+-- of the `X` bundle corresponding to the `subX` structure/bundle
+-- being defined here.
+
 open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup)
 
 private
   module G = AbelianGroup G
 
+-- Here, we could chose simply to expose the `NormalSubgroup` definition
+-- from `Algebra.Construct.Sub.Group.Normal`, but as this module will use
+-- type inference to allow the creation of `NormalSubgroup`s based on their
+-- `isNormal` fields alone, it makes sense also to export the type `IsNormal`.
+
 open import Algebra.Construct.Sub.Group.Normal G.group
   using (IsNormal; NormalSubgroup)
 
@@ -24,25 +40,39 @@ 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
+-- * it is, in fact, Normal
+-- * and defines an AbelianGroup, not just a Group
 
 module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where
 
+-- Here, we do need both the underlying function `ι` of the mono, and
+-- the proof `ι-monomorphism`, in order to be able to construct an
+-- `IsAbelianGroup` structure on the way to the `AbelianGroup` bundle.
+
   open Subgroup subgroup public
     using (ι; ι-monomorphism)
 
-  abelianGroup : AbelianGroup c′ ℓ′
-  abelianGroup = record
-    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
-
-  open AbelianGroup abelianGroup public
+-- Here, we eta-contract the use of `G.comm` in defining the `normal` field.
 
   isNormal : IsNormal subgroup
   isNormal = record { normal = λ n → G.comm (ι n) }
 
+-- And the use of `record`s throughout permits this 'boilerplate' construction.
+
   normalSubgroup : NormalSubgroup c′ ℓ′
   normalSubgroup = record { isNormal = isNormal }
 
+-- And the `public` re-export of its substructure.
+
   open NormalSubgroup normalSubgroup public
     using (conjugate; normal)
+
+-- As with `Algebra.Construct.Sub.Group`, there seems no need to create
+-- an intermediate manifest field `isAbelianGroup`, when this may be, and
+-- is, obtained by opening the bundle for `public` export.
+
+  abelianGroup : AbelianGroup c′ ℓ′
+  abelianGroup = record
+    { isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
+
+  open AbelianGroup abelianGroup public

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

@@ -57,7 +57,8 @@ record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ
 
 -- As with `Subgroup` itself, this domain `Carrier` type is canonically inferrable
 -- by the typechecker, as in the inline comment. But perhaps this use of `_` might
--- also be usefully documented as `Function.Base.typeOf n`?
+-- also be usefully documented as `Function.Base.typeOf n`? Or is that itself too
+-- 'occult' a usage?
 
     conjugate : ∀ n g → _ -- where _ = RawGroup.Carrier (Subgroup.domain subgroup)
 
@@ -68,7 +69,7 @@ record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ
 
     normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
 
--- NormalSubgroup: a Subgroup which IsNormal (sic)
+-- NormalSubgroup: a Subgroup which IsNormal (sic).
 
 record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
@@ -85,3 +86,12 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh
 
   open Subgroup subgroup public
   open IsNormal isNormal public
+
+-- NB. Nowhere does this module define, nor need to, the lemma introduced in
+-- Taneb's original PR, viz. `abelian⇒subgroup-normal` of type
+-- `Commutative G._≈_ G._∙_ → (subgroup : Subgroup _ _) → IsNormal subgroup`.
+--
+-- This element of reasoning is itself handled by having a distinct module
+-- `Algebra.Construct.Sub.AbelianGroup` which encapsulates such reasoning
+-- within the scope of (an `Abelian`!)`Group` `G` in which the premise
+-- `Commutative G._≈_ G._∙_` is already known to hold.