Add negatives for commutative monoids and semirings (Abelian group and ring completions)

[LionOfJewdah]

Summary

• add Algebra.Construct.Add.Negatives.CommutativeMonoid, constructing formal differences of a commutative monoid with a slack-balance setoid relation
• add Algebra.Construct.Add.Negatives.Semiring, extending the additive completion with the semiring multiplication
• reuse the direct-product commutative-monoid laws and prove multiplication congruence structurally via left and right scalar actions on formal differences
• provide the canonical monoid and semiring homomorphisms, the commutative-ring specialization, and decomposition into positive and negative parts
• prove that an absorbing additive element makes the group completion trivial, and consequently forces 1# ≈ 0# in the ring completion
• prove that the completion of an Abelian group or ring is canonically isomorphic to the original group or ring

Motivation

These modules provide reusable group and ring completions without relying on the algebra solver. The carrier reuses Algebra.Construct.DirectProduct; the proofs use setoid equational reasoning, product combinators, and existing algebra-property lemmas.

Validation

• fix-whitespace --check CHANGELOG.md src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda src/Algebra/Construct/Add/Negatives/Semiring.agda
• agda --safe --ignore-interfaces -Werror +RTS -M6G -A128M -RTS -i src src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda
• agda --safe --ignore-interfaces -Werror +RTS -M6G -A128M -RTS -i src src/Algebra/Construct/Add/Negatives/Semiring.agda
• regenerated and checked EverythingSafe with the same safety, warning, and RTS flags
• checked a concrete smoke module instantiating the ring completion with the natural-number semiring and exercising both self-completion isomorphisms

[LionOfJewdah]

I didn't do it yet, but I could add if desired that if the monoid / semigroup is already a group / ring, its completion is isomorphic to itself with (a, b) -> a - b

Edit: Now I did it

[jamesmckinna]

Notwithstanding existing mathematical terms-of-art, I'd probably reckon that Completion is too generic a word to capture these particular Algebra.Constructs... so, at the risk of verbosity, suggest perhaps CommutativeCompletion? At least at the module name level, to aid discoverability. or Grothendieck but we tend not to use personal names for concepts, except in comments.

[LionOfJewdah]

How about InverseCompletion or NegativeCompletion? Alternatively, Algebra.Construct.Add.Negatives, probably still in subfiles like now, as opposed to one file.
And yes, Grothendieck in a comment would be good, something like "Group completion of a commutative monoid, i.e. the monoid's Grothendieck group"

[LionOfJewdah]

(Also I just realized I can reuse more of the proofs from Algebra.Construct.DirectProduct directly, like +-assoc, so I'll save a lot of lines that way in the next iteration.)

[jamesmckinna]

As to where things (should) live, I sort of agree with Algebra.Construct.Add.* but the extra level of nesting (esp. when done on a per-algebra basis) is quite annoying, to me at least. I think that @JacquesCarette and @MatthewDaggitt may have better ideas about where such things should live,

[jamesmckinna]

Re: equational reasoning proofs

See also Algebra.Properties.Monoid (and upwards) for additional principles which obtain as the axiomatisation increases in strength... so that for example many of the rearrangement lemmas may already be covered by existing combinators.

[jamesmckinna]

Re: force-pushing branches (Happy to be corrected on matters git-related)

As I understand it, this makes it harder (if not impossible, without directly accessing individual commits?) to survey the history of an evolving PR, even at the barebones level of satisfying reviewers that requested/suggested changes have been taken into account ...

... but at a less adversarial level, my experience is that, absent more serious attempts to document our development process(es), PR history can still provide valuable insight into the evolution of ideas, esp. design ideas, as well as a(n admittedly highly diffuse) archive of 'learning resources' for the community, esp. future developers and maintainers.

[LionOfJewdah]

My apologies on the git force pushes -- I'm a software engineer and this is common at my employer. It's not universally done, and I'll refrain from doing it with stdlib contributions.

Regarding rearrangement lemmas and other monoid properties, on that now.

Would you prefer this be one file or two?

[jamesmckinna]

Regarding file-level organisation as modules, 2 seems easier to grasp right now, but I haven't had time to sit down and do a serious review (yet), so I can't really say definitively for the now...

[JacquesCarette]

I wonder, how much of the CommutativeMonoid completion can re-use the Semiring completion? Or is it a sufficiently different construction that basically none can be?

[JacquesCarette]

I don't think pos and neg should be exported from this construction.

[JacquesCarette]

perhaps slack should be on the left, so that when it is 0, cancellation is free?

I wonder if there should be a 'tight' equivalence also defined, i.e. without the slack.

[JacquesCarette]

Have to wonder if using G. instead of all these renamings would be just as clear?

[JacquesCarette]

Maybe comment as to why the slack now has to be explicit? I think I can figure it out, but the next reader shouldn't have to!

[JacquesCarette]

As to where it should live: I find the current choice pretty good, actually! Yes, the nesting is deep, but this is a reflection that the library is getting larger.

[LionOfJewdah]

I'm working on the latest feedback.

I also realized two things:

1. I didn't include semimodules, which of course become modules on the ring completion.
2. I didn't include the universal homomorphisms M -> G or S -> R from the monoid/semiring into any Abelian group/ring factoring through the embedding

On semimodules:

• Should it be in this PR or a follow up?
• Should it be under Algebra.Construct like these or Algebra.Module.*?
• How general should it go? Just two sided semimodules of the same semiring, left and/or right semimodules of a given semiring, bimodules of two possibly different semirings, etc?

On the universal property:

• How much, if any, should go in this PR or a follow up?
• The factorization of the morphisms is tractable, but uniqueness requires an equivalence relation on homomorphisms that I'm not sure exists yet in stdlib (though I'd love to be wrong), pointwise setoid equality.
• Such a congruence relation would also support proofs of natural and integer initiality among (semi-)rings, which if desired, I would want to contribute in a later PR for scope concerns

I forget the path in stdlib, but I know there's already an action module for the naturals on any monoid. I forget if there is for the integers and groups.