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

Stream: Is there code for X?

[Scott Morrison]

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]

(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.)

[Kenny Lau]

is there a canonical module structure?

[Scott Morrison]

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.

[Scott Morrison]

#2759