Stream: Is there code for X?
Scott Morrison (May 20 2020 at 10:47):
Do we have somewhere:
variables (R : Type*) [comm_ring R] (S : Type*) [ring S] [algebra R S] (V : Type*) [add_comm_group V] [module S V] (W : Type*) [add_comm_group W] [module S W] def linear_map_algebra_module : module R (V →ₗ[S] W) := sorry
I'm not finding it so far, but perhaps it hasn't been done.
Scott Morrison (May 20 2020 at 10:48):
R modules, we have an instance for
module R (V →ₗ[R] W), and of course it's just not true that there is a
module S (V →ₗ[S] W) instance at all.)
Kenny Lau (May 20 2020 at 10:49):
is there a canonical module structure?
Scott Morrison (May 20 2020 at 10:51):
You just define
(r • f) v = f (r • v), and use that fact that
r commutes with everything in
S to check that this is still an
Scott Morrison (May 20 2020 at 11:49):
Last updated: May 07 2021 at 21:10 UTC