Algebras should imply both left and right actions

[eric-wieser]

TL;DR: we need an instance from Algebra R A to Module Rᵐᵒᵖ A, and it needs to not create diamonds.

The problem

Mathematically, an $R$-algebra $A$ ([CommSemiring R] [Semiring A] [Algebra R A]) has an obvious action by the commutative $R$. If pushed, we can say that it has obvious left- and right- actions, corresponding to $(r : A)a$ and $a(r : A)$.

However, we can't (and don't) implement things this way in Lean; if we do so, then we end up with instance diamonds, where r • a from some prexisting module structure is not equal to the one defined via the algebra as algebraMap R A r * a.
We've already solved this for left actions; we did this by:

• Making Algebra extend SMul
• Adding Algebra.smul_def to prove that these operations coincide propositionally.
• Adding Algebra.toModule which provides the rest of the algebraic structure, but constructs no new data.

However, mathlib now also has various results about right actions (written Module Rᵐᵒᵖ A), specially left- and right- actions that are compatible in some way. One example is:

instance TrivSqZeroExt.monoid
  {R : Type u} {M : Type v}
  [Monoid R] [AddMonoid M]
  -- M is acted on by `R` on both the left and the right, and the actions associate:
  -- $(r_1 m) r_2 = r_1 (m r_2)$
  [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :
  Monoid (TrivSqZeroExt R M)

This presents a difficulty; this instance can't be applied when M is an Algebra, as there is no instance from Algebra R A to Module Rᵐᵒᵖ A.

Another notable example is Derivation, which if generalized in the same way (as in leanprover-community/mathlib#18936) would cease to be usable on commutative rings.

The solution

A solution to this in Lean3 is at leanprover-community/mathlib#10716, which passed CI but was never merged.

The summary is that Algebra needs to gain:

• A SMul Rᵐᵒᵖ A field, to provide the new data needed to make things diamond free
• An Algebra.op_smul_def' x r : op r • x = x * toFun r proof field that shows this is consistent with multiplication
• Adding an instance Algebra.toOppositeModule which provides the rest of the algebraic structure, but constructs no new data.
• Adding an instance Algebra.isCentralScalar : IsCentralScalar R A which follows trivially from Algebra.commutes

This unfortunately creates a new problem: for Algebra ℕ R over some ring, we now need a right-action of ℕ on R, that is defeq to right-multiplication when R = ℕ. Once again, we solved this for left-modules with the AddMonoid.nsmul field; we need to do the same for AddMonoid.op_nsmul. Overall, we will need to add:

• AddMonoid.op_nsmul (and AddMonoid.op_nsmul_eq_nsmul)
• SubtractionMonoid.op_zsmul (and SubtractionMonoid.op_zsmul_eq_zsmul)
• DivisionRing.op_qsmul (and DivisionRing.op_qsmul_eq_qsmul)

Unfortunately, these first two need to match up with the additive versions; so we also need to add op_pow and op_zpow versions too!

[alreadydone]

What do you think about introducing

class RightAlgebra (R A) [CommSemiring R] [Semiring A] [Algebra R A] extends SMul Rᵐᵒᵖ A where
  op_smul_def' (x : A) (r : R) := op r • x = x * algebraMap R A r

and use it whenever we want to consider the right action of a base ring on an algebra? It's not that different from

class foo (R A) [SMul R A] extends SMul Rᵐᵒᵖ A, IsCentralScalar R A

but may or may not be more performant; bundling should be more performant than adding [SMul Rᵐᵒᵖ A] [IsCentralScalar R A] as arguments separately.

I always disliked mathlib's forgetful inheritance approach that bundle lots of stuff into classes (e.g. now MetricSpace includes UniformSpace and Bornology, and UniformSpace extends TopologicalSpace, but it's rarely the case that we really need to use all those structures at once), which doesn't seem very extendible and scalable, and think we should extract compatibility classes out of them. Another example I have in mind is matroids, which has lots of equivalent definitions in terms of different data (the buzzword is "cryptomorphism"). Maybe we can start experimenting with an alternative approach in noncommutative algebra.

[eric-wieser]

As a short-term workaround that approach looks ok (as does just adding [SMul Rᵐᵒᵖ A] [IsCentralScalar R A]) but mathematically it's annoying because those are always satisfied by an algebra, and it feels like saying "an algebra that is really an algebra"