Add subgroups and submodules

[Taneb]

Pulled out of work on #2729 that can be merged straight away hopefully

[jamesmckinna]

This all looks great (esp. following our discussion this morning).

My only (cosmetic) hesitation is/would be over the field name Sub in each case, but in truth I don't have an improvement over it.

Cut! Print!

[JacquesCarette]

I think the name Algebra.Construct.Sub.* is fine, even good. I think the name Sub as a field name is not.

group ? Because it is a group, it has an independent existing as a group, and acquires a new one when inserted into this record.

[Taneb]

I'm willing to change the name but I don't like the name group - there's already another group lurking in the background and I'm worried they'll be confused

[JacquesCarette]

Fair. I'll try to come up with other suggestions. (I did not propose rawgroup because I dislike that quite a bit myself.)

[Taneb]

Looking what I actually wrote, I use group for the embellishment of Sub with laws

[JacquesCarette]

in a similar vein, I would want module, but that can't work. moduleOn, since it is parametrized?

[jamesmckinna]

I agree with @JacquesCarette that Sub is a bad name, but earlier I came up short trying think of a better one. But let's try harder!

It occurs to me that, in one sense, the name cannot matter, as we could insist that it only ever be accessed as the underlying (computed) rawGroup manifest field of the group manifest field of Subgroup, but that may be too much cognitive gymnastics for most readers/users...

... I've argued, persuasively or not, for 'canonicalising' the name \iota for the (name of the) monomorphism defining the subobject, so it would be good to have a canonical name for its domain (and not to be fussy about standardising apart each such name according to what algebraic signature/structure it is intended to support; that's handled by the manifest field names)... so how about:

• domain (I'm largely indifferent to capitalisation, but I can see Domain as perhaps preferable)
• subobject (a marginal improvement on Sub? ditto. re capitalisation)
• ... I (this might cause trouble!? but hints we should take care when referring to it... and we definitely need capitalisation here!)
• Iota (or even \Iota!?)

I realise this is a vexed topic, and I want to stress the last two are not intended vexatiously (nor facetiously); we need a name for a thing which shouldn't really ever be referred to directly outwith the record declaration. Choosing a 'jarring' field name might be a way to achieve that?

Avoiding prior convention, Freyd/Sčedrov in their Categories/Allegories book, used prefix and suffix 'box' on (names of arrows) to denote 'domain' and 'codomain' (with moreover the advantage of being minimum-ink), so \box\iota could work, I suppose.

Early morning thoughts of a chronic insomniac!

[Taneb]

domain was something I was thinking of suggesting.

Another suggestion: H (for group) or N (for module), i.e. the second dummy variable name for the structure

[jamesmckinna]

domain was something I was thinking of suggesting.

OK, good to maybe achieve some convergence on this?

Another suggestion: H (for group) or N (for module), i.e. the second dummy variable name for the structure

yes, that would be very much in the spirit of old-school typographical convention in mathematics,

(sidebar: did we actually get this from mathematicians, or from the extraordinarily gifted typesetters/printers at, particularly, Oxford University Press, Springer, and Van Nostrand Reinhold, who left such a mark on published Anglophone/German mathematics in the pre-digital, pre- frantic M&A consolidation years ie up to about 1980?)

but as @JacquesCarette often points out, we need to move past such orthodoxies, and if we're going to keep the same name for the monomorphism, then we need to keep the same name for its domain? (eyes on a generative solution downstream, cf. #2287 etc.)

[Taneb]

I've changed the name from Sub to domain, but the name of the (private) module Sub to H/N

[jamesmckinna]

This may be the sweet spot... the internal module names are private, so the one-character name doesn't violate #2472 ... while the potentially-exportable name domain is consistently repeatable and sufficiently distinct ... looks good to me!

[Taneb]

I've realised that later on in my development of modular arithmetic, I don't want sub modules per se, but sub R-R-bimodules (I don't want to assume that R is commutative). Or possibly sub left (eq. right) modules.

[jamesmckinna]

Hmmm... but that could be added downstream, or else (easily?) as part of this one?

[jamesmckinna]

What's the reason for not including the versions also for Module? Eventually we'll want all of these things?