Right action equals left action

Stream: Is there code for X?

[Oliver Nash]

Do we have this lemma anywhere:

import Mathlib.LinearAlgebra.Basic

@[simp] lemma MulOpposite.smul_eq_smul {R M : Type _} [Monoid R] [SMul R M] [MulAction Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower R Rᵐᵒᵖ M] (x : R) (m : M) :
    MulOpposite.op x • m = x • m :=
  calc MulOpposite.op x • m = (1 * MulOpposite.op x) • m := by rw [one_mul]
                          _ = (x • (1 : Rᵐᵒᵖ)) • m := rfl
                          _ = x • ((1 : Rᵐᵒᵖ) • m) := by rw [smul_assoc]
                          _ = (1 : Rᵐᵒᵖ) • (x • m) := by rw [smul_comm]
                          _ = x • m := by rw [one_smul]

[Oliver Nash]

(Informally it says that IsScalarTower R Rᵐᵒᵖ M is the condition for an R-R-bimodule to be really just a left (say) module.)

[Jireh Loreaux]

Isn't this docs#IsCentralScalar ?

[Oliver Nash]

OK docs#IsCentralScalar is the way to make this statement and I have here a proof that this instance arises from IsScalarTower R Rᵐᵒᵖ M (subject to the other assumptions). Thanks!

[Jireh Loreaux]

We don't need to worry about type class loops anymore, right? Or do we? If we do, I'd be concerned you're about to create one.

[Oliver Nash]

I believe we don't and thus could maybe add:

import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.RingTheory.Derivation.Basic

instance {R M : Type _} [Monoid R] [SMul R M] [MulAction Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower R Rᵐᵒᵖ M] : IsCentralScalar R M := by
  constructor
  intro x m
  calc MulOpposite.op x • m = (1 * MulOpposite.op x) • m := by rw [one_mul]
                          _ = (x • (1 : Rᵐᵒᵖ)) • m := rfl
                          _ = x • (1 : Rᵐᵒᵖ) • m := smul_assoc x 1 m
                          _ = (1 : Rᵐᵒᵖ) • x • m := smul_comm x 1 m
                          _ = x • m := by rw [one_smul]

[Jireh Loreaux]

I can't find the other instance I expected might exist anyway, so I think it's fine either way.

[Oliver Nash]

But now that you've drawn my attention to docs#IsCentralScalar I don't really need this anymore :)

[Oliver Nash]

Thanks!

[Oliver Nash]

I do think docs#IsCentralScalar.op_smul_eq_smul should be simp though.

[Eric Wieser]

The other direction of the loop is that IsCentralScalar R M implies some of the ᵐᵒᵖ tower instances

[Eric Wieser]

Oliver Nash said:

I do think docs#IsCentralScalar.op_smul_eq_smul should be simp though.

This seems reasonable; I think I was just trying to be conservative.

[Oliver Nash]

Let's see if #5346 builds!