# The monoidal closed structure on Module R. #

noncomputable def ModuleCat.monoidalClosedHomEquiv {R : Type u} [] (M : ) (N : ) (P : ) :
( P) (N (.obj { unop := M }).obj P)

Auxiliary definition for the MonoidalClosed instance on Module R. (This is only a separate definition in order to speed up typechecking. )

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance ModuleCat.instMonoidalClosed {R : Type u} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem ModuleCat.ihom_map_apply {R : Type u} [] {M : } {N : } {P : } (f : N P) (g : (ModuleCat.of R (M N))) :
(.map f) g =
theorem ModuleCat.monoidalClosed_curry {R : Type u} [] {M : } {N : } {P : } (f : ) (x : M) (y : N) :
x = f (x ⊗ₜ[R] y)
@[simp]
theorem ModuleCat.monoidalClosed_uncurry {R : Type u} [] {M : } {N : } {P : } (f : N .obj P) (x : M) (y : N) :
(x ⊗ₜ[R] y) = (f y) x
theorem ModuleCat.ihom_ev_app {R : Type u} [] (M : ) (N : ) :
.app N = (TensorProduct.uncurry R (M) (M →ₗ[R] N) N) LinearMap.id.flip

Describes the counit of the adjunction M ⊗ - ⊣ Hom(M, -). Given an R-module N this should give a map M ⊗ Hom(M, N) ⟶ N, so we flip the order of the arguments in the identity map Hom(M, N) ⟶ (M ⟶ N) and uncurry the resulting map M ⟶ Hom(M, N) ⟶ N.

theorem ModuleCat.ihom_coev_app {R : Type u} [] (M : ) (N : ) :
.app N = (TensorProduct.mk R { unop := M }.unop (.obj N)).flip

Describes the unit of the adjunction M ⊗ - ⊣ Hom(M, -). Given an R-module N this should define a map N ⟶ Hom(M, M ⊗ N), which is given by flipping the arguments in the natural R-bilinear map M ⟶ N ⟶ M ⊗ N.

theorem ModuleCat.monoidalClosed_pre_app {R : Type u} [] {M : } {N : } (P : ) (f : N M) :
P = LinearMap.lcomp R (P) f