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!

[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!

[jamesmckinna]

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

[Taneb]

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

The principle of "only adding only what I need immediately". I worry that if this becomes the "add every possible sub-whatever" PR it'll take about a month to get done

[jamesmckinna]

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

The principle of "only adding only what I need immediately". I worry that if this becomes the "add every possible sub-whatever" PR it'll take about a month to get done

Absolutely fair enough. I was only surpised that given you did have working code for the other case, it might have been easier to leave it in. Definitely not asking for the full tapestry of subXYZmodules!

[jamesmckinna]

Happy to merge now, but I'd be happier still if the module imports/private blocks were tidied up in the spirit of the style-guide... but I think we can nitpick all of that downstream in round (n+1) of library refactoring...

[Taneb]

I'd rather fix the style points before this gets merged. I should be able to do that today

[jamesmckinna]

Suggested change

	private
	module G = Group G
	open import Algebra.Structures using (IsGroup)
	open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
	import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism
	open import Level using (suc; _⊔_)
	open import Algebra.Structures using (IsGroup)
	open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
	import Algebra.Morphism.GroupMonomorphism as GroupMonomorphism
	open import Level using (suc; _⊔_)
	private
	module G = Group G

[jamesmckinna]

Suggested change

	module Algebra.Module.Construct.Sub.Bimodule {cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) where
	module Algebra.Module.Construct.Sub.Bimodule
	{cr ℓr cs ℓs cm ℓm} {R : Ring cr ℓr} {S : Ring cs ℓs} (M : Bimodule R S cm ℓm) where

[Taneb]

Styleguide says if you're splitting the module declaration, where should be on its own line

[jamesmckinna]

touch'e!

[jamesmckinna]

Suggested change

	private
	module R = Ring R
	module S = Ring S
	module M = Bimodule M
	open import Algebra.Construct.Sub.Group M.+ᴹ-group
	open import Algebra.Module.Structures using (IsBimodule)
	open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
	import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism
	open import Level using (suc; _⊔_)
	open import Algebra.Module.Structures using (IsBimodule)
	open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
	import Algebra.Module.Morphism.BimoduleMonomorphism as BimoduleMonomorphism
	open import Level using (suc; _⊔_)
	private
	module R = Ring R
	module S = Ring S
	module M = Bimodule M
	open import Algebra.Construct.Sub.Group M.+ᴹ-group

[jamesmckinna]

Comment (no action required):
if I ever get my way with #2252 then this would simplify to

  isBimodule : IsBimodule R S domain

which... I would see as a win ;-)

[jamesmckinna]

I (still; further) don't want to get in the way of this PR, but I think that given that the Algebra.Module.* definitions all assume commutativity of the underlying additive structure on which the *Ring multiplication variously acts, that this could usefully be refactored once #2854 gets merged so that:

• Subgroups of AbelianGroups are automatically Normal (moreover directly, not going via abelian⇒subgroup-normal)
• hence, Sub*modules (of Ring-based *modules; perhaps there's a story to tell about Semi such things, with an underlying CommutativeMonoid?) are automatically Normal
• and, Quotients of AbelianGroups need only take a Subgroup as second argument to the construction
• hence Ideals are automatically Normal, and thus give rise to suitable quotients, without having to relitigate the abelian quotient structure
• ... etc.

Accordingly, it's tempting to suggest adding Algebra.Construct.Sub.Group, Algebra.NormalSubgroup, and Algebra.Construct.Sub.AbelianGroup first, and only then add Subbimodule and Algebra.Ideal... but as I say, this could be a downstream refactoring instead... cf. #2854 (comment)

[JacquesCarette]

still looking good to me.

[jamesmckinna]

Still looking good, and it would be good to merge, but what's happening with the cosmetic fix-ups @Taneb ?