comment: the design of Ideal

Author: jamesmckinna

src/Algebra/Construct/Sub/Ring/Ideal.agda

@@ -2,12 +2,19 @@
 -- The Agda standard library
 --
 -- Ideals of a ring
+--
+-- Based on Nathan van Doorn (Taneb)'s original PR
+-- https://github.com/agda/agda-stdlib/pull/2855
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
 open import Algebra.Bundles using (Ring)
 
+-- As with `Algebra.Construct.Sub.Group.Normal`, this module
+-- relocates Taneb's original `Algebra.Ideal`
+-- to a level one *below* that of `Algebra.Construct.Sub.Ring`.
+
 module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where
 
 open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
@@ -16,10 +23,17 @@ open import Level using (suc; _⊔_)
 
 ------------------------------------------------------------------------
 -- Definition
--- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
+--
+-- A (two sided) ideal is exactly a sub-bimodule of R, considered as
+-- a bimodule (the `TensorUnit` for that category) over itself.
 
 record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
     subbimodule : Subbimodule {R = R} bimodule c′ ℓ′
 
+-- The definition of `Subbimodule` now exports the `normalSubgroup`
+-- and `abelianGroup` definitions, so that a `Ring` modulo an `Ideal`
+-- already has direct access to the underlying quotient `(Abelian)Group`
+-- structure on the additive group of the ring.
+
   open Subbimodule subbimodule public

src/Algebra/Module/Construct/Sub/Bimodule.agda

@@ -8,9 +8,10 @@
 -- but uses the `Algebra.Construct.Sub.AbelianGroup` module
 -- to plumb in that any sub-bimodule of a `Bimodule` defines
 -- a sub-AbelianGroup, hence a `NormalSubgroup`, so that when
--- an ideal in a `Ring` is defined as a suitable sub-bimodule,
+-- an `Ideal` in a `Ring` is defined as a suitable sub-bimodule,
+-- as in https://github.com/agda/agda-stdlib/pull/2855
 -- the quotient structure of the additive subgroup is immediate,
--- on which the quotient `Ring` structure may then be defined.
+-- on which the quotient `Ring` structure may then be based.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}