restrict scalars of linear map

Stream: maths

[Johan Commelin]

If I have an R-algebra A and an A-linear map f : M -> N. How do I turn f into an R-linear map?

[Johan Commelin]

Presumably this should use is_scalar_tower.

[Kenny Lau]

docs#is_scalar_tower.restrict_base

[Johan Commelin]

Aha, that's for alg_homs. I need the analogue for linear maps.

[Johan Commelin]

But this shows how it should be done.

[Johan Commelin]

How do I turn an A-module into an R-module?

[Johan Commelin]

Is this not yet in mathlib?

[Adam Topaz]

Isn't this docs#semimodule.restrict_scalars ?

[Johan Commelin]

Aha, I guess it is.

[Johan Commelin]

Thanks

[Adam Topaz]

As far as I know, mathlib does not have the restriction of scalars for modules along a morphism of arbitrary (possibly noncommutative) (semi)rings. I would be happy to be wrong about that.

[Johan Commelin]

I'm doing everything commutative atm (-; And using algebras...