[ add ] Algebra.Construct.Centre.X of an algebra X, following #2863

[jamesmckinna]

This PR is a clean do-over of #2863 , avoiding any dependency/coupling on either #2872 or #2854 .

Issues:

• keeps the 'iterated' design from [ add ] Centre of a Group etc. #2863 ie. the centre of a Group is defined in terms of the centre of its underlying Monoid, iterated down as far as a bare Center Centre type based on the (components of) an underlying RawMagma.
• doesn't explicitly plumb in the construction of Sub.X (eg as in [ draft ] Alternative design for sub- and quotient- (Abelian)Groups #2859 ) until the discussion on that PR and Normal subgroups and quotient groups #2854 stabilises with an agreed hierarchy for such sub-algebras.
• can (easily) be refactored when and if [ add ] Relation.Binary.Morphism.Construct.On #2872 and/or [ rename/deprecate ] Rename Algebra.Properties.Monoid.ε-comm #2883 get merged, etc. UPDATED: DONE
• there's probably a lot more that can be done to simplify/refactor Algebra.Construct.Centre.Ring (and develop the infrastructure for the 'missing' intermediate algebras...)

NB. the hierarchy of IsXMonomorphism structures unfortunately (;-)/!?) goes against the grain of how these things are all built up successively here, so downstream we might think about refactoring that hierarchy, or else introducing more 'smart' constructors for such things.

[JacquesCarette]

Only change needed: delete commented out code.

[jamesmckinna]

This is ready to go, so if someone is willing either to offer an additional review, or else support merging as-is, please do so!

[JacquesCarette]

I guess we need to explicitly ping people like @Taneb and @MatthewDaggitt since I've already done my part!

[jamesmckinna]

So hopefully I've now dealt with the feedback above, EXCEPT:

• trying to unpack isRingHomomorphism exposes that the exports of Ring fail to capture all the necessary nested records
• that I'm not convinced that writing out all the sub-records makes sense (discuss?)
• BUT that it might also be useful to explicitly export a bundled XMonomorphism from Z[ X ] to X (but we've never quite resolved to date where the unique morphisms arising from Algebra.Construct.Y should live?)

I suggest it's better to tackle these downstream!

UPDATED: I've now been persuaded to take a more maximalist approach to exports ... not clear to me, until these constructions are exercised in anger, that we see exactly what is and is not necessary here.

[JacquesCarette]

I'm still good on this. Only need @gallais to re-review.

[jamesmckinna]

@gallais back to you now...