[ draft ] Alternative design for sub- and quotient- (Abelian)Groups
#2859
Conversation
| { isMonoid = record | ||
| { isSemigroup = record | ||
| { isMagma = record | ||
| { isEquivalence = record |
There was a problem hiding this comment.
I know this is just an experiment, but I'd certainly with that this IsEquivalence record was pulled out.
| record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where | ||
| open Subgroup subgroup using (ι) | ||
| field | ||
| conjugate : ∀ n g → _ |
There was a problem hiding this comment.
That _ is perverse. Sure, it can be reconstructed -- so what? Record declarations serve as documentation too!
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Definition | ||
| -- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself |
There was a problem hiding this comment.
minor: sub-bimodule please. I find 'subbimodule' very hard to parse (as a human) properly.
| open AbelianGroup abelianGroup public | ||
|
|
||
| isNormal : IsNormal subgroup | ||
| isNormal = record { normal = λ n → G.comm (ι n) } |
|
I'm sure this alternative design makes a lot of sense to you @jamesmckinna and to @Taneb , but since I don't have the original in mind, your description relative to it does not really inform me in any substantial way of the pros and cons of each. i.e. could the PR description be made less relative to knowing the original, but rather have more information about both designs in the description please? |
2 participants
Alternative to #2852 and #2854 , based on @Taneb's original design, but:
Normalis now belowAlgebra.Construct.Sub.GroupAlgebra.Construct.Sub.AbelianGroups added, and are automaticallyNormalHence:
Algebra.Module.Construct.Sub.Bimodules are automatically suitable asIdealsAlgebra.Construct.Sub.RingAlgebra.Construct.Quotient.Ring