## Stream: maths

### Topic: restrict scalars of linear map

#### Johan Commelin (Oct 21 2020 at 09:38):

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 (Oct 21 2020 at 09:38):

Presumably this should use is_scalar_tower.

#### Kenny Lau (Oct 21 2020 at 09:39):

docs#is_scalar_tower.restrict_base

#### Johan Commelin (Oct 21 2020 at 09:41):

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

#### Johan Commelin (Oct 21 2020 at 09:41):

But this shows how it should be done.

#### Johan Commelin (Oct 21 2020 at 14:28):

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

#### Johan Commelin (Oct 21 2020 at 14:28):

Is this not yet in mathlib?

#### Adam Topaz (Oct 21 2020 at 14:31):

Isn't this docs#semimodule.restrict_scalars ?

#### Johan Commelin (Oct 21 2020 at 14:34):

Aha, I guess it is.

Thanks

#### Adam Topaz (Oct 21 2020 at 14:39):

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 (Oct 21 2020 at 14:39):

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

Last updated: May 10 2021 at 07:15 UTC