[ draft ] Alternative design for sub- and quotient- `(Abelian)Group`s

[jamesmckinna]

Alternative to #2852 and #2854 , based on @Taneb's original design, but:

• Normal is now below Algebra.Construct.Sub.Group
• Algebra.Construct.Sub.AbelianGroups added, and are automatically Normal

Hence:

• downstream, Algebra.Module.Construct.Sub.Bimodules are automatically suitable as Ideals
• ... below Algebra.Construct.Sub.Ring
• simplifying Algebra.Construct.Quotient.Ring

The high-level differences between the two approaches mostly consist in:

• this one is more aggressively optimised than @Taneb 's original in the spirit of #2391 , in terms of making large single definitions of nested records, and opening them to expose substructure
• in avoiding, wherever possible, redundant imports/type signatures solely for the sake of making explicit the types of 'implementation details', so that the resulting (public) API for the various constructions is (or at least aims to be) as abstract as possible from a client perspective
• exact location of concepts within the Algebra hierarchy, and their mutual dependency (aiming to flatten/linearise the latter, and making the former follow a more conventional inheritance based directory/sub-directory tree structure
• making the notion of 'sub-Abelian group' explicit, and using that to streamline the development of sub- and quotient- structure of richer algebras (such as Ring) which are based on an underlying (additive) Abelian group structure, which slightly alters the conceptual, as well as concrete dependency graph compared to Taneb's #2852 #2854 and #2855

[JacquesCarette]

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?

[jamesmckinna]

I think that the best answer to the above comment might be to give a more detailed commentary in the source? (See ongoing/recent commits)

I think that this is probably more portable/surveyable than a complex interweaving of the GitHub comment trail? This still seems to be a major bugbear in using git to debate alternatives, and to document discussion around such things, as we have observed in the past, elsewhere in this project.

[jamesmckinna]

@JacquesCarette regarding the Algebra.Construct.Sub 'mis-identification', sadly this is also present in #2852 (now merged), so we should do some retrofitting if you want to distinguish the

• hierarchy of SubX definitions (Magma, Monoid, Group, Ring...)
• hierarchy of SubX constructions (CommutativeMagma, CommutativeMonoid, AbelianGroup, CommutativeRing...)

I guess I took at face value that we 'construct' a subgroup by supplying a monomorphism... but I see your point. It's (potentially) a lot more complicated to do so, so we perhaps need to discuss further with @Taneb on a fresh issue/PR?

[JacquesCarette]

Re: Algebra.Construct.Sub 'mis-identification', and #2852 -- those are not yet released, so there is still time!

And yes, I hope that @Taneb will chyme in soon. I think it is worthwhile to use different terminology to indicate "definition" and "construction". I was happy to see that in Voevodsky's later work, he was quite careful in labelling things, including making this difference.