Zulip Chat Archive

Stream: maths

Topic: restrict scalars of linear map


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 21 2020 at 09:38):

Presumably this should use is_scalar_tower.

view this post on Zulip Kenny Lau (Oct 21 2020 at 09:39):

docs#is_scalar_tower.restrict_base

view this post on Zulip Johan Commelin (Oct 21 2020 at 09:41):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 09:41):

But this shows how it should be done.

view this post on Zulip Johan Commelin (Oct 21 2020 at 14:28):

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

view this post on Zulip Johan Commelin (Oct 21 2020 at 14:28):

Is this not yet in mathlib?

view this post on Zulip Adam Topaz (Oct 21 2020 at 14:31):

Isn't this docs#semimodule.restrict_scalars ?

view this post on Zulip Johan Commelin (Oct 21 2020 at 14:34):

Aha, I guess it is.

view this post on Zulip Johan Commelin (Oct 21 2020 at 14:34):

Thanks

view this post on Zulip 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.

view this post on Zulip 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