Zulip Chat Archive

Stream: Is there code for X?

Topic: linear maps between algebra modules form a module over ...


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

view this post on Zulip Scott Morrison (May 20 2020 at 10:48):

(If V and W are 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.)

view this post on Zulip Kenny Lau (May 20 2020 at 10:49):

is there a canonical module structure?

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

view this post on Zulip Scott Morrison (May 20 2020 at 11:49):

#2759


Last updated: May 07 2021 at 21:10 UTC