[ add ] Centre of a Group etc.

[jamesmckinna]

Modulo spelling... ;-)

Currently: blocked on #2854 / #2859
Need to rebase against #2854 ?

TODO: add/refactor to use

• Semigroup
• Monoid
• Ring
• ...
• Magma seems not to make sense, because no assoc, but definition of Central/Center make sense without?

UPDATED: refactor to make use of #2872 #2873

[JacquesCarette]

As a Canadian whose idea of spelling is an ungodly mixture of American and English, I will refrain on opining between Centre and Center. (But it is colour, for sure.)

[JacquesCarette]

Very shallow review (but it is a draft).

I find the code duplication between the definitions of Centre appalling. It may well be Agda's fault.

[JacquesCarette]

semi-facetiously: Magma or RawSemigroup ?

But actually: one has the data of the equivalence being a congruence, the other does not. So if you're going to go 'minimal', maybe RawMagma rather than Magma?

[jamesmckinna]

Well, OK... I dithered a lot about whether to even have an entry at this level of the hierarchy... but it seemed the best place to 'hide' the definition of Center, so that it is never subsequently explicit referred to except via its ι; central; ι-isXMonomorphism interface.

But in the absence of associativity, it is ridiculous at some level to have this. Above Magma (ie Semigroup and beyond), we do need assoc, so it doesn't really make sense to avoid also cong etc.? But maybe we should consider 'central' notions only wrt the underlying Raw structure throughout? is that what you're suggesting?

As for RawSemigroup, well we don't have it, because that just 'is' (would be) RawMagma (as in the IsXHomomorphism hierarchy, which only uses IsRawX structures to drive the definitions, and rightly so).

But, yes: draft, so come back at me down the road!

[jamesmckinna]

I find the code duplication between the definitions of Centre appalling. It may well be Agda's fault.

(not sure I quite understand?)

Actually, I was trying to avoid code duplication, by exporting Center etc. publicly through the hierarchy. Is there an alternative approach? When I started with Group, everything was in one place, so the 'inheritance' hierarchy wasn't clear. What I've tried to do here is

• identify the 'local' increment at each stage (I could even do this in a private block, to avoid export...?)
• identify the global increment for export at each stage wrt the *-IsHomomorphism properties and bundles

I welcome suggestions for a better design! (Maybe my modelling skills need sharpening for the Algebra hierarchy?)

The thing which makes me sad is re-duplication of the injective proofs... but that could be fixed with a suitably shadow hierarchy of smart constructors for *-IsMonomorphism, ... which we haven't developed yet. Maybe we should (sigh...).

UPDATED: I now think I agree, and it seems to be express itself in my having to re-export not only Center etc., but also the ∙-comm proof as well, when I'd rather be able to inherit the commutativeY sub-bundle straightaway when defining the commutativeX bundles, but that may be because the SubX hierarchy isn't quite right yet, either... Advice welcome!

[jamesmckinna]

As a Canadian whose idea of spelling is an ungodly mixture of American and English, I will refrain on opining between Centre and Center. (But it is colour, for sure.)

Busted!

As a UK-English user, I've embodied by cultural preference in the folder/module-name hierarchy, while in deference to US-English for mathematical concepts, I have the formal object Center... which I then try to avoid referring to in terms of the public exported API ;-)

[jamesmckinna]

Looping back to @JacquesCarette 's

I find the code duplication between the definitions of Centre appalling. It may well be Agda's fault.

There may be a way out of this via #2876 and keeping all the definitions inside one (nested) module, so the that 'nested/iterated' re-export is less painful.

I think that means that I should return to this later, once some of the other infrastructural PRs have landed.