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

jamesmckinna · 2025-11-05T14:29:15Z

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 [DRY] what's the best way to publicly re-export properties/structure? #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 Add subgroups and submodules #2852 Normal subgroups and quotient groups #2854 and Add ideals and quotient rings #2855

JacquesCarette · 2025-11-08T19:41:57Z

src/Algebra/Construct/Quotient/Group.agda

+    { isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = record


I know this is just an experiment, but I'd certainly wish that this IsEquivalence record was pulled out.

One thing that impressed me about @Taneb 's code was the extent to which, in various places, it manages to produces huge nested record blocks which nevertheless 'do the right thing'.

I've flip-flopped over the years between this style, and a much more incremental, define every sub-record at top-level, put the pieces together step-by-step style, which the library has to date favoured.

One reason (perhaps two or more!) I am now turning towards the 'one big record' style arises from #2391 :

a single large object, suitably re-opened as public, (re-)introduces all the 'correct' substructure, moreover with the 'rectified'/'official' names, rather than trying to invent proxy names for the top-level substructure in the other style

when any client imports the new constructions, they aren't faced with a (DRY) choice between cherry-picking the ad-hoc names (which may be the 'correct' ones), or facing a clash/choicepoint between such names and those names introduced by open of substructures

In this instance (as perhaps elsewhere...) the definition of distinct isEquivalence : IsEquivalence ... fields at top-level is starting to emerge as an anti-pattern for me: once an Algebra.Structures.IsX object is in scope, or has been defined, then isEquivalence is available as a canonical projection from that, and indeed that should be the preferred mode-of-access (via open if necessary) for a substructure which exists solely

to export canonical names refl, sym, trans for the properties, and their derived forms

to construct Setoids from which Relation.Binary.Reasoning.Setoid syntax may then be brought into scope

...

... much of which functionality/behaviour can be achieved at a higher-level of the nesting hierarchy by suitable re-organisation of the Algebra.Properties.X hierarchy #2804 #2858 etc.

Defining every sub-record independently also gets out of hand. I've settled on an approach more 'in the middle' where some particularly re-usable records are given top-level names.

The big record always exists, so users can choose that one if that's what they want, or the big one and open it.

I guess I was thinking of the "developer API" here rather than the "user API". So I think that's where our difference of opinion comes from, we had different modes of use in mind.

This is where natural language and Agda are insufficiently precise.

JacquesCarette · 2025-11-08T19:45:48Z

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

+record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
+  open Subgroup subgroup using (ι)
+  field
+    conjugate : ∀ n g → _


That _ is perverse. Sure, it can be reconstructed -- so what? Record declarations serve as documentation too!

Thanks for "perverse"... ;-)

I surely agree that

record declarations should be self-documenting
but, here, I think that

an-line comment would here do as much work in explaining why a name isn't necessary...

... rather than, as now, having to introduce a private manifest field defining a module (or else expose a new name for a subfield of the subgroup object), solely for the sake of projecting out the name of its Carrier.

So... at rock-bottom, I chose this design as a optimisation for space (as well as that of my cognitive load, but it seems YMMV) and like all such, doing this prematurely might be harmful.

But as with the comment above about isEquivalence, I am starting to find that when we create/open substructures of this sort, it is usually in a context in which the 'missing'/'hidden' name of the type is already in scope with another pre-existing name which is more salient in that deployment context.

So the private module name, and or that of its sub-fields, is being created solely for the purpose of documentation.

Accordingly, in this setting, I made a design choice to avoid committing to creating such an 'ephemeral' name. But an inline comment should, I think, solve this problem?

I'd still be OK if you disagreed with my above thought process (which should, in any case, be documented towards any eventual codification of a library-design philosophy ;-)), and I guess part of the point of offering an 'alternative' design for these fundamantal structures was to create an opportunity for debate around such questions.

I think I would be sufficiently placated with an inline comment.

I ended up just being explicit, and saving the indirection... ;-)

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

JacquesCarette · 2025-11-08T19:47:10Z

src/Algebra/Construct/Sub/AbelianGroup.agda

+  open AbelianGroup abelianGroup public
+
+  isNormal : IsNormal subgroup
+  isNormal = record { normal = λ n → G.comm (ι n) }


eta contract?

Yes! In that, it is itself an eta-contraction of the original

isNormal = record { normal = λ n g → G.comm (ι n) g }

Is it harmful to have done this?

Or are you asking whether the definition could be contracted further? Perhaps, but only via one of those odd Function.Base composition operators which compose only in one argument position of an n+2-ary function, which I find obscure rather than illuminate (my point-free fu is not always as strong as it might be).

Oh, I had not noticed that this had been contracted once already! I was thinking that this would be a straightforward composition. Hmm, now I wonder if the eta expanded version isn't easier to understand!

Could be: but work on #2863 suggests that this, plus commutativity in the Centre constructions, might better be plumbed in by other means. Further experimentation required!

JacquesCarette · 2025-11-08T19:50:09Z

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 · 2025-11-09T09:26:16Z

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 · 2025-11-11T03:21:27Z

src/Algebra/Construct/Sub/Group.agda

+-- which is already inherited (by definitional equality!) from the type of
+-- the `⟦_⟧` parameter to `IsXHomomorphism`...
+
+    ι              : _ → G.Carrier -- where _ = RawGroup.Carrier domain


A last thought on this (or two, depending on how you count; maybe it's 3/2 of a thought): either of the following would also typecheck:

Suggested change

ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain

ι : _ → _

or

Suggested change

ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain

ι : _ -- where _ = RawGroup.Carrier domain → G.Carrier

JacquesCarette

I do really like the extensive documentation.

I think some modules are in the 'wrong' place (see detailed comments).

JacquesCarette · 2025-11-11T23:46:41Z

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

+-- 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


But why is this under Construct? This defines what being a Normal Subgroup is -- it does not construct anything!

Algebra.Gropu.Sub.Normal ?

Well, it's under Sub.Group... so if that moves, so too will/should this.

JacquesCarette · 2025-11-11T23:49:08Z

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

+-- to a level one *below* that of `Algebra.Construct.Sub.Ring`,
+-- notwithstanding that we have yet to define `Sub.XRing`s...
+
+module Algebra.Construct.Sub.Ring.Ideal {c ℓ} (R : Ring c ℓ) where


Same comment about this file not containing a construction but rather a definition. And it isn't Sub either: an Ideal is defined as a property of a Ring R. This happens to use a Sub-bimodule as part of its definition, sure, but it is not a Subring. So I think both Construct and Sub don't belong in the name.

Yeah, I wondered about this.
Do we regard NormalSubgroup, Ideal etc. as 'special' kinds of Subobject?
Or is the specialness that hey give rise to Quotients?
I'd previously suggested to @Taneb a Quotientable hierarchy, and then Quotient.X takes an X and a Quotientable.X as parameters... but got pushback on that idea.

#2854 and #2855 put these things at the top of Algebra, and that doesn't seem right to me either.

JacquesCarette · 2025-11-11T23:52:40Z

src/Algebra/Construct/Sub/AbelianGroup.agda

+
+open import Algebra.Bundles using (AbelianGroup)
+
+module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where


This is better named: it does construct an AbelianGroup out of a (normal) subgroup. This seems like it is in the right place.

Yes (but still: sigh).

JacquesCarette · 2025-11-11T23:53:35Z

src/Algebra/Construct/Sub/Group.agda

+
+open import Algebra.Bundles using (Group; RawGroup)
+
+module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where


Again: this does not Construct anything, it gives a definition. So Sub fits, Construct does not.

Inherited from #2852 so we've got some retrofitting to do...

jamesmckinna · 2025-11-12T10:20:19Z

@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?

jamesmckinna added 3 commits November 5, 2025 14:10

refactor: alternative to agda#2852 and agda#2854

e2ff677

refactor: alternative to agda#2852 and agda#2854

f702f82

add: sub-Bimodules

bd5cfee

jamesmckinna added addition library-design refactoring labels Nov 5, 2025

jamesmckinna marked this pull request as draft November 5, 2025 14:29

jamesmckinna requested review from JacquesCarette and Taneb November 5, 2025 14:29

jamesmckinna added 3 commits November 5, 2025 14:31

fix: whitespace

d3d6797

add: Ideals and quotients of Rings

c05773b

fix: tidy up

b707d83

This was referenced Nov 6, 2025

Normal subgroups and quotient groups #2854

Open

Add ideals and quotient rings #2855

Draft

[ add ] Centre of a Group etc. #2863

Closed

JacquesCarette requested changes Nov 8, 2025

View reviewed changes

jamesmckinna added 9 commits November 9, 2025 10:23

comment: extensively on the design rationale

3a75f5f

comment: extensively on NormalSubgroup (sic)

4d72ed0

comment: extensively on AbelianSubgroup

18d99ef

comment: extensively on Subbimodule

882c56c

comment: the design of Ideal

bc146da

comment/refactor: Ideal

3ac84f3

refactor: simplify Quotients

6522369

refactor: more on Group

6778d54

update: CHANGELOG

08560e2

jamesmckinna commented Nov 11, 2025

View reviewed changes

JacquesCarette requested changes Nov 11, 2025

View reviewed changes

jamesmckinna mentioned this pull request Nov 12, 2025

[ bug/refactor ] fix spurious dependencies in Algebra.Morphism.*Monomorphism #2870

Open

4 tasks

	ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain
	ι : _ → _

	ι : _ → G.Carrier -- where _ = RawGroup.Carrier domain
	ι : _ -- where _ = RawGroup.Carrier domain → G.Carrier


		open import Algebra.Bundles using (AbelianGroup)

		module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where


		open import Algebra.Bundles using (Group; RawGroup)

		module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where

[ draft ] Alternative design for sub- and quotient- (Abelian)Groups #2859

Are you sure you want to change the base?

[ draft ] Alternative design for sub- and quotient- (Abelian)Groups #2859

Uh oh!

Conversation

jamesmckinna commented Nov 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette Nov 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Nov 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Nov 8, 2025

Uh oh!

jamesmckinna commented Nov 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Nov 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Nov 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

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

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

jamesmckinna commented Nov 5, 2025 •

edited

Loading

JacquesCarette Nov 8, 2025 •

edited

Loading

jamesmckinna Nov 9, 2025 •

edited

Loading

jamesmckinna commented Nov 9, 2025 •

edited

Loading

jamesmckinna Nov 12, 2025 •

edited

Loading