Commit 2024-11-14 11:25 e62619b1

feat(SkewMonoidAlgebra): add SkewMonoidAlgebra with irreducible def (#15878)

Skew Monoid algebras

This file presents a skewed version of Mathlib.Algebra.MonoidAlgebra.Basic with an irreducible definition.

Context

Hi everyone, As a part of a bigger project aiming to get Drinfeld Modules into Mathlib, @María Inés de Frutos Fernández and I have been trying to get a generalization of MonoidAlgebra, SkewMonoidAlgebra, into Mathlib. The first attempt at this was #10541, but progress has been slow as making the definition irreducible caused a huge refactor. Following @kbuzzard's suggestion, I am opening this PR which contains only the first 160 lines of #10541. In particular, this PR is missing most of what makes these objects skewed (Multiplication was defined only at line 558 as it requires stronger hypotheses and there are many lemmas on the additive structure that precede it.) This means that the purpose of this PR is mainly to get the separation from Finsupp right. Please consult this thread for more context or in short: The current separation we have consists of:

Wrapping the definition with a structure.
Making basic operations such as add private and irreducible.
Adapting relevant definitions.
Copying and adapting relevant theorems from the base construct to obtain statements in terms of our new object. Is this what everyone has in mind? If so, are there parts of the current PR that come short in respect to any of these? I am happy to integrate suggestions to improve the separation if there are any! Thanks a lot for your attention and help! Xavier