LinearMap.CompatibleSMul instance

Stream: Is there code for X?

[Edison Xie]

Do we have this in mathlib and is this the right generality?

import Mathlib

instance compatible (k A M1 M2 : Type*) [CommRing k] [Ring A] [Algebra k A]
    [AddCommGroup M1] [Module k M1] [Module A M1] [AddCommGroup M2] [Module A M2]
    [IsScalarTower k A M1] :
    letI := Module.compHom M2 (algebraMap k A)
    LinearMap.CompatibleSMul M1 M2 k A :=
  letI := Module.compHom M2 (algebraMap k A)
  ⟨fun f k m ↦ by rw [algebra_compatible_smul A, map_smul]; rfl⟩

[Kenny Lau]

Edison Xie said:

is this the right generality

surely they can be semirings

[Kevin Buzzard]

docs#Module.compHom

[Kevin Buzzard]

Why not just ask for [Module k M2] [IsScalarTower k A M2]? In situations where Module k M2 already exists and is not defeq to Module.compHom you might be in trouble with this instance as it stands

[Andrew Yang]

docs#IsScalarTower.compatibleSMul

[Edison Xie]

Kevin Buzzard said:

Why not just ask for [Module k M2] [IsScalarTower k A M2]? In situations where Module k M2 already exists and is not defeq to Module.compHom you might be in trouble with this instance as it stands

the context is that I'm trying to cleanup some old proofs from my brauer group repo to try and PR them, since none of the rings in there is commutative and I often have to "choose" a simple module over a simple ring it's not at all trivial to me that it may satisfy "IsScalarTower" :-(

[Edison Xie]

but after some work I proved IsScalarTower instance so thanks for the suggestion :-)

[Edison Xie]

Andrew Yang said:

docs#IsScalarTower.compatibleSMul

do you mean docs#LinearMap.IsScalarTower.compatibleSMul ?

[Andrew Yang]

The is scalar tower instance should be .of_algebraMap_smul fun _ _ => rfl