Commit 2026-07-04 08:56 61303857

refactor(Algebra): make MonoidAlgebra into a one-field structure (#38714) Replace

def MonoidAlgebra (R M : Type*) [Semiring R] : Type _ := M →₀ R

by

structure MonoidAlgebra (R M : Type*) [Semiring R] where
  ofCoeff :: coeff : M →₀ R

and similarly for AddMonoidAlgebra. Since elements of MonoidAlgebra R M shouldn't be considered as finitely supported functions M → R anymore, I also remove the coercion to functions. This is a major change with many ramifications in mathlib. The foremost consequence is that it is now by design impossible to abuse defeqs by using Finsupp API on MonoidAlgebra. There are more consequences:

1. coeff is now used very widely. Many lemma names are renamed to contain coeff since their type signature changed.
2. For convenience, I copy more Finsupp API over to MonoidAlgebra. This includes induction principles (induction) and linear combinations (supported).
3. The existing API copied over from Finsupp has no reason to be so through abbrev (anymore?/ever), so I make them defs instead.
4. Many equalities in MonoidAlgebra that were previously obtained through direct applications of the relevant Finsupp lemmas are now replaced by ext; simp.
5. Many set_option backward.isDefEq.respectTransparency false are removed and a similar (but slightly smaller) number are added, essentially because we are pushing further the boundary of abuse. In many cases, the easiest solution to something breaking was to rid it of its own abuse. Therefore the following that changes that are a priori orthogonal to the titular change were made:
6. Make PolynomialModule a one-field structure, similarly to MonoidAlgebra.
7. Deduce the MvPolynomial base change results from the AddMonoidAlgebra ones. In particular, the AddMonoidAlgebra ones take the base ring on the left while the MvPolynomial ones took it on the right. Left is the correct side because of how heterogeneous base change is set up in mathlib.
8. Make the representation theory library use MonoidAlgebra more, whereas previously it was using MonoidAlgebra and Finsupp interchangeably.
9. Add ModuleCat.monoidAlgebraFree as an alternative to ModuleCat.free that uses MonoidAlgebra instead of Finsupp. This is useful to fix homological results that broke due to point 3. Some points that are left as future work:
10. Polynomial R is currently defined as a one-field structure around AddMonoidAlgebra R ℕ. Pending performance, it could become an abbrev instead.
11. MonoidAlgebra could become an abbrev of SkewMonoidAlgebra since it is a special case of it. In fact, SkewMonoidAlgebra could itself become a special case of CrossProductAlgebra from BrauerGroup.
12. MvPowerSeries and PowerSeries should follow the same treatment as MonoidAlgebra.
13. Finsupp should become an abbrev of (non-dependent) DFinsupp. This becomes easier after the current PR since the Finsupp API is used much less widely.