comment: extensively on NormalSubgroup (sic)

Author: jamesmckinna

src/Algebra/Construct/Sub/Group.agda

@@ -36,51 +36,52 @@ private
 record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
 
--- as above, this name is essentially arbitrary,
--- exisitng solely to be mentioned in the third field below
+-- As above, the following name is essentially arbitrary, existing
+-- solely to be mentioned in the third field `ι-monomorphism` below.
 
     domain         : RawGroup c′ ℓ′
 
--- this function (obviously) needs a source and target:
--- * the target, for the sake of the third field, needs to be
---   `Carrier` subfield of the top-level `X` module parameter
+-- The next field, a function, (obviously) needs a source and target:
+-- * the target, again for the sake of the third field, needs to be
+--   `Carrier` subfield of the top-level `X` module parameter;
 -- * the source, however, really exists solely to give a type to `ι`
---   and indeed, the typechecker can infer (from the third field)
---   that this type *must* be the `Carrier` of the `RawX` `domain`
+--   and indeed, the typechecker can infer (again from the third field)
+--   that this type *must* be the `Carrier` of the `RawX` `domain`.
 
 -- Taneb's design introduces a `private` module
 -- `private module H = RawGroup domain`
 -- for the sake of affording easy/easier named access to its
 -- `Carrier` field, and as preferable to the hideous explicit form
--- `RawGroup.Carrier domain` which is the definiens of `H.Carrier`
+-- `RawGroup.Carrier domain` which is the definiens of `H.Carrier`.
 
--- Neither is necessary, but can be, and is, reconstructed by the
--- typechecker by offering instead a placeholder, in exactly the same way
+-- Neither is necessary, but instead can be, and is here, reconstructed by
+-- the typechecker by offering instead a placeholder, in exactly the same way
 -- that `domain` exists as a named field solely to express the dependency
 -- in the type of `ι-monomorphism`. In that sense, it is an ephemeral form
--- derived from `domain`, which moreover will never play a role in client
--- uses of this module, except as a typing constraint on any application
--- of `ι`, a constraint which is already inherited (by definitional equality!)
--- from the type of the `⟦_⟧` parameter to `IsXHomomorphism`...
+-- derived from `domain`, which moreover will *never* play a role in client
+-- uses of this module (eg exemplarily in `Algebra.Construct.Sub.Group.Normal),
+-- except as a typing constraint on any application of `ι`, a constraint
+-- which is already inherited (by definitional equality!) from the type of
+-- the `⟦_⟧` parameter to `IsXHomomorphism`...
 
     ι              : _ → G.Carrier -- where _ = RawGroup.Carrier domain
 
--- now all the pieces are in place, we can define what we *really* want
+-- Now all the pieces are in place, we can define what we *really* want:
 
     ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
 
--- this is 'admin': any client module of `Subgroup` will likely want to
--- refer to primitive *and* manifest subfields of `IsXMonmorphism`, so
--- this is automatically made available to clients, but not `open`ed,
--- so that such affordance is client-definable, as usual.
+-- The next manifest field is an 'admin' decision: any client module of
+-- `Subgroup` will likely want to refer to primitive *and* manifest subfields
+-- of `IsXMonomorphism`, so this is automatically made available to clients,
+-- but not `open`ed, so that such affordance is client-definable, as usual.
 
   module ι = IsGroupMonomorphism ι-monomorphism
 
 -- Similarly, but mathematically motivated: any client module of `Subgroup`
 -- will want access to *the `X` defined as the domain of the `IsXMonomorphism`*.
 -- But here, it is both automatically made available to clients, as above,
 -- *and* also `open`ed, so that its affordances are offered to any client
--- via the 'canonical' names associated with the `X`/`IsX` bundle/structure
+-- via the 'canonical' names associated with the `X`/`IsX` bundle/structure.
 
 -- Taneb's design does this in two steps:
 -- * first, create the `IsX` structure, with name `isX`

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

@@ -2,31 +2,86 @@
 -- The Agda standard library
 --
 -- Definition of normal subgroups
+--
+-- Based on Nathan van Doorn (Taneb)'s original PR
+-- https://github.com/agda/agda-stdlib/pull/2852
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
 open import Algebra.Bundles using (Group)
 
+-- This module relocates Taneb's original `Algebra.NormalSubgroup`
+-- to a level one *below* that of `Algebra.Construct.Sub.Group`,
+-- for the 'obvious' inheritance hierarchy 'reason' that a
+-- `NormalSubgroup` is a specialisation of the notion of `Subgroup`.
+
+-- `Normal` as a root name avoids recapitulation of the parent name
+-- `Subgroup`, but also permits/does not frustrate development of a
+-- companion `Construct` sub-hierarchy (intersections etc.) below
+-- `Algebra/Construct/Sub/Group/Normal` as a sub-directory.
+
 module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ)  where
 
 open import Algebra.Construct.Sub.Group G using (Subgroup)
+open import Function.Base using (typeOf)
 open import Level using (suc; _⊔_)
 
 private
   module G = Group G
 
--- every element of the subgroup commutes in G
+------------------------------------------------------------------------
+-- Definition
+--
+-- IsNormal: every element of the given subgroup commutes in the parent.
+--
+-- This defined as a `record`, as usual in order to improve type inference,
+-- specifically that a `NormalSubgroup` below may (usually) be definable
+-- solely by supplying its `isNormal` field.
+
 record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
+
+-- A design question here is how much of the `Subgroup` structure should/must
+-- be exposed in the course of defining the fields here.
+
+-- Surely we need the name of the function which witnesses 'subX'-ness,
+-- but not the property `ι-isXMonomorphism`.
+
   open Subgroup subgroup using (ι)
+
   field
-    conjugate : ∀ n g → _
+
+-- But it's not obvious that we need the (name of) `Carrier` of the `domain`
+-- of the `Subgroup`, viz. the source of `ι`, except as the type of variables
+-- quantifed here as `n` (as generic name for 'element's of the normal subgroup).
+
+-- 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`?
+
+    conjugate : ∀ n g → _ -- where _ = RawGroup.Carrier (Subgroup.domain subgroup)
+
+-- The main field of interest only requires that the `conjugate` field be
+-- of type 'source of `ι`'; but we don't need that type here, otherwise the
+-- `∀ n` quantifier would need an explicit type label, and such inferrability
+-- reinforces the decision nowhere to name this type.
+
     normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
 
+-- NormalSubgroup: a Subgroup which IsNormal (sic)
+
 record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
     subgroup : Subgroup c′ ℓ′
     isNormal : IsNormal subgroup
 
+-- But again, and for generic `library-design` reasons, we publicaly export
+-- all the subfields of each field, in order to afford a standardised vocabulary
+-- for all the structure intended to be in scope when using a `NormalSubgroup`.
+
+-- Locally, we have used only name `ι` in the definition of `IsNormal`,
+-- but clients may also want access ot the full signature (eg. esp. the
+-- `ι-isGroupMonomorphism` field which characterises being a subgroup).
+
   open Subgroup subgroup public
   open IsNormal isNormal public