Separate `Finsupp` from `AddMonoidAlgebra`

Stream: mathlib4

[Damiano Testa]

The plan is to place the structure divide when defining AddMonoidAlgebra, right? I remember that @Eric Wieser had suggested even trying to unify AddMonoidAlgebra and MonoidAlgebra: these two refactors should not happen at the same time!

(conversation started here).

[Damiano Testa]

I envisage a process where

• we introduce the divide in a branch,
• we fix some of the proofs that break in Mathlib,
• we stop when we get bored or there are no further proofs to fix, at which point, we also introduce the divide in Mathlib.

Does this sound reasonable?

[María Inés de Frutos Fernández]

@Xavier Généreux and I are working on a generalization of MonoidAlgebra, SkewMonoidAlgebra, in #10541 (which we would also need to refactor analogously). We only did the multiplicative version, partly because some of our results in the skewed case rely on MulSemiringAction.

[Damiano Testa]

Ok, thanks for the heads up! Since I think that this will be a somewhat long process, I do not see a big issue with starting it with AddMonoidAlgebra and then seeing when/where to extend.

[María Inés de Frutos Fernández]

Damiano Testa said:

@Eric Wieser had suggested even trying to unify AddMonoidAlgebra and MonoidAlgebra.

There is an implementation note in MonoidAlgebra.Basic which seems related to this:

Similarly, I attempted to just define k[G] := MonoidAlgebra k (Multiplicative G), but the definitional equality Multiplicative G = G leaks through everywhere, and seems impossible to use.

Would unifying the two classes lead to problems with polynomials?

[Damiano Testa]

María, yes, this is related to the unification. I am less confident about this change, so my plan is to start with defining

structure AddMonoidAlgebra where ofFinsupp ::
  toFinsupp : G →₀ k

instead of the current

def AddMonoidAlgebra :=
  G →₀ k

[María Inés de Frutos Fernández]

OK, sounds good.

[Antoine Chambert-Loir]

Can you explain what this modification should change?

[Kevin Buzzard]

It would break some proofs where definitonal abuse was occurring, and this might be a good thing because definitonal abuse can contribute to leakage. The point is that the dictionary between the two concepts will now be toFinsupp or \<_\> whereas right now it's id

[Yaël Dillies]

And mostly we get back the mathematical identity between AddMonoidAlgebra and Polynomial

[Yaël Dillies]

Polynomial are just a special-case of monoid algebras, and should be formalised as such.

[Damiano Testa]

It also moves the separation between Finsupp and Polynomial at the place where the "real" difference is, namely where multiplication starts being used.

[Antoine Chambert-Loir]

Except that I think there should exist a “monoid module” - at least if M acts on V, an action of the monoid algebra of M (Finsupp M k) on (Finsupp V k).

[Xavier Généreux]

Hello everyone,
Following the discussion of this thread, I have updated #10541 that introduces a generalisation of MonoidAlgebra, SkewMonoidAlgebra, to match the change described above. Are there any updates on whether this change is still happening/planned? I would like to build on the current version of SkewMonoidAlgebra of #10541, in particular by defining SkewPolynomial.

[Damiano Testa]

I have not given up on the split, but AddMonoidAlgebra and MonoidAlgebra are not parallel enough. So, I am trying to first make them really parallel and then change only one, with the other auto-changed.

You can see some partial progress at #12637.