Add `Algebra.Definitions.RawGroup` and `Algebra.Properties.Group.*`

[jamesmckinna]

On the model of

• Algebra.Definitions.RawMonoid
• Algebra.Properties.Monoid.*

Introducing the 'obvious' action(s) of type ℤ → Carrier → Carrier.

Plus: additional properties in the AbelianGroup case...

[JacquesCarette]

Should it really be for ℤ or for any structure that has FOO properties?

[Taneb]

@JacquesCarette what do you mean by "FOO properties"?

[jamesmckinna]

@JacquesCarette Yes, I agree, but as with the Nat action (by multiplication) for (Raw)Monoid, it first seems superficially tied to the action of the free FOO (if I understand that usage correctly).

But then we should go back and refactor the Nat (and Bool) Semiring actions for monoids. What's the best evolutionary path to follow? A mega PR doing things 'right', or else piecemeal, as in the current proposal?

And: let's agree a design for Free things, so that Nat as the free Semiring, and Z as the free Ring, on no generators, can be characterised as such... #1962
The more I pull on these threads... the more unravels!

[JacquesCarette]

@Taneb I meant it as a placeholder variable for something like Semiring, or whatever structure+property bundle is necessary to meaningfully define the concept.

Re: evolution. I'm starting to wonder if we need a companion library that builds on top of stdlib but has no strong compatibility guarantees, so that it may evolve much faster. For stdlib: I think mega PRs are very dangerous; then tend to go stale and never land. So I prefer piecemeal, so that progress actually happens. The problem with that is that mistakes might creep in to 'piecemeal' only to be discovered just-too-late. Thus my thoughts about a more experimental on-top library.

Yes, a design for Free things is likely timely.

I don't see it so much as 'threads unraveling' as (re)discovering that mathematics is internally very structured. (We're not the only ones, Rocq and Lean people are (re)discovering the same, but not necessarily in the same spots.)

[jamesmckinna]

@JacquesCarette Lots of food-for-thought in your last comments... hypothetical-rewrite redux?
And as to "mathematics is internally very structured"... yes, the various modern experiments with libraries seem to recapitulate, in yet-further new ways, that there is no single, 'best', Bourbachiste solution, in spite of our more illustrious forebears in this regard?