Star modules over non-commutative scalars

Stream: maths

[Oliver Nash]

I think our definition docs#StarModule is not right if the scalars are not commutative. We should have the axiom $(r \cdot a)^* = a^* \cdot r^*$ rather than $(r \cdot a)^* = r^* \cdot a^*$. In particular, I claim this is a concept for bimodules.

[Oliver Nash]

Or in Lean I claim the "right" definition should be:

class StarModule (R A : Type _) [Star R] [Star A] [SMul R A] [SMul Rᵐᵒᵖ A] :=
  star_smul : ∀ (r : R) (a : A), star (r • a) = (MulOpposite.op (star r)) • a

[Oliver Nash]

However burdening every user with the obligation to supply an Rᵐᵒᵖ action seems like a bad idea so I propose keeping the "wrong" axiom but restricting the typeclass to require a commutative multiplication.

[Oliver Nash]

Any remarks / corrections welcome!

[Eric Wieser]

I think I claimed this some time ago :)

[Oliver Nash]

Two steps ahead as always :)

[Oliver Nash]

I'm not really affected by this but I'll try and do something about it in a few days if nobody else does.

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Is.20star_module.20sensible.20for.20non-commutative.20rings.3F/near/257272767

[Eric Wieser]

I think there's a big obstacle here, and it's that Algebra R A does not imply SMul Rᵐᵒᵖ A

[Eric Wieser]

I spent quite some time fixing that in Lean3, but the PR (!3#10716) went stale

[Oliver Nash]

I'm proposing that we deal with this the way we currently deal with docs#Derivation: we restrict typeclasses so that the definition can only be used in the commutative case, when it is actually correct.