Automatic isScalarTower instances

Stream: Is there code for X?

[Antoine Chambert-Loir]

If S is an R-algebra and M is an S-module, it is tempting to view M as an R-module, together with an IsScalarTower R S M instance but mathlib doesn't seem to be aware of that.
When trying to define it, as follows,

def Algebra.toModule (R S M : Type*) [CommSemiring R] [Semiring S] [Algebra R S]
    [AddCommMonoid M] [Module S M] : Module R M where
  smul r m := algebraMap R S r • m
  one_smul m := by
    change algebraMap R S 1 • m = m
    simp
  mul_smul r s m := by
    change algebraMap R S (r * s) • m = algebraMap R S r • (algebraMap R S s) • m
    simp [mul_smul]
  smul_zero r := by
    change algebraMap R S r • (0 : M) = 0
    simp
  smul_add r m n := by
    change algebraMap R S r • (m + n) = algebraMap R S r • m + algebraMap R S r • n
    simp
  add_smul r s m := by
    change algebraMap R S (r + s) • m = algebraMap R S r • m + (algebraMap R S s) • m
    simp [Module.add_smul]
  zero_smul m := by
    change algebraMap R S (0 : R) • m = 0
    simp

def Algebra.toIsScalarTower (R S M : Type*) [CommSemiring R] [Semiring S] [Algebra R S]
    [AddCommMonoid M] [Module S M] :
    @IsScalarTower R S M _ _ (Algebra.toModule R S M).toSMul := by
  let _ : Module R M := Algebra.toModule R S M
  apply IsScalarTower.mk
  intro r s m
  change _ = (algebraMap R S) r • s • m
  rw [smul_smul, Algebra.smul_def]

I need to do a lot of tedious change, and there should (is there) a better way…

[Junyan Xu]

docs#RestrictScalars is the type synonym that carries the desired instance RestrictScalars.isScalarTower

[Eric Wieser]

There's also docs#Module.compHom