Normal subgroups and quotient groups #2854
Conversation
jamesmckinna
left a comment
jamesmckinna
left a comment
There was a problem hiding this comment.
This all looks great. I've made suggestions, but nothing is a deal-breaker.
Taneb
force-pushed
the
quotient-groups
branch
from
8d0576a to
65c4224
Compare
Taneb
force-pushed
the
quotient-groups
branch
from
65c4224 to
e3baf59
Compare
| private | ||
| module N = NormalSubgroup N | ||
| open NormalSubgroup N using (ι; module ι; conjugate; normal) |
There was a problem hiding this comment.
Can simplify this to:
| private | |
| module N = NormalSubgroup N | |
| open NormalSubgroup N using (ι; module ι; conjugate; normal) | |
| private | |
| open module N = NormalSubgroup N using (ι; module ι; conjugate; normal) |
| project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project | ||
| project-isHomomorphism = record |
There was a problem hiding this comment.
Naming?
| project-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project | |
| project-isHomomorphism = record | |
| project-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project | |
| project-isGroupHomomorphism = record |
Twofold reasons:
- Subsequently, for
Ring R / Ideal I, you also defineproject-isHomomorphism : IsRingHomomorphism, and maybe that's enough (let theXpath context of the algebra determine what kind ofIsXHomomorphismis defined - BUT, for
Ring, what you actually need is to separate out theisMonoidHomomorphismfield, so why not alsoisGroupHomomorphism?
| open import Algebra.Morphism.Structures using (IsGroupHomomorphism) | ||
| open import Algebra.Properties.Monoid monoid | ||
| open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙) | ||
| open import Algebra.Structures using (IsGroup) |
There was a problem hiding this comment.
Do we need this import? Cf. #2391 and see below.
| } | ||
|
|
||
| quotientGroup : Group c (c ⊔ ℓ ⊔ c′) | ||
| quotientGroup = record { isGroup = quotientIsGroup } |
There was a problem hiding this comment.
And now inline the definition above?
| quotientGroup = record { isGroup = quotientIsGroup } | |
| quotientGroup = record | |
| { isGroup = ... | |
| } |
|
In lieu of any further review comments, please see #2859 (purely!) as a comparison point, and feel free to grab anything from there which you might find useful... it just seemed the easiest way to encapsulate all the thoughts I had had about your groups-rings-modules development |
Taneb
force-pushed
the
quotient-groups
branch
from
2460cf0 to
b481327
Compare
I noted that every time I used normal it was under sym This felt like a good reason to reverse it
Taneb
force-pushed
the
quotient-groups
branch
from
998fe3d to
d5c518b
Compare
| infix 0 _by_ | ||
|
|
||
| data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where | ||
| _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y |
There was a problem hiding this comment.
If this is instead _by_ : ∀ g → x ∙ ι g ≈ y → x ≋ y some things line up nicer when we get to integers (in particular it matches Data.Integer.DivMod.a≡a%n+[a/n]*n)
There was a problem hiding this comment.
Well, so be it, but be careful of having a tail wag the dog. It wouldn't be the first time that existing stdlib modules expose argument order/definitional inconsistency when exposed to new additions/refactoriings (the saga of Algebra.Properties.*.Divisibility and Data.Nat.DivMod.* being a case in point)...
There was a problem hiding this comment.
The alternative here would be putting more lemmas in Data.Integer.DivMod, which I want to do anyway
|
FTR, if you don't feel like augmenting this with the |
Builds off #2852, continuing towards #2729 in bitesize chunks.