# mathlib3documentation

algebra.category.Module.monoidal.closed

# The monoidal closed structure on Module R. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def Module.monoidal_closed_hom_equiv {R : Type u} [comm_ring R] (M N P : Module R) :
(N .obj (opposite.op M)).obj P)

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

Equations
@[simp]
theorem Module.monoidal_closed_hom_equiv_symm_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : N .obj (opposite.op M)).obj P) :
P).symm) f = (β_ M N).hom
@[simp]
theorem Module.monoidal_closed_hom_equiv_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : P) :
P) f = M).compr₂ ((β_ N M).hom f)
theorem Module.ihom_map_apply {R : Type u} [comm_ring R] {M N P : Module R} (f : N P) (g : (M N))) :
.map f) g = g f
@[simp]
theorem Module.monoidal_closed_curry {R : Type u} [comm_ring R] {M N P : Module R} (f : M N P) (x : M) (y : N) :
= f (x ⊗ₜ[R] y)
@[simp]
theorem Module.monoidal_closed_uncurry {R : Type u} [comm_ring R] {M N P : Module R} (f : N P) (x : M) (y : N) :
(x ⊗ₜ[R] y) = (f y) x
theorem Module.ihom_ev_app {R : Type u} [comm_ring R] (M N : Module R) :

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 Module.ihom_coev_app {R : Type u} [comm_ring R] (M N : Module R) :
= ((𝟭 (Module R)).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 Module.monoidal_closed_pre_app {R : Type u} [comm_ring R] {M N : Module R} (P : Module R) (f : N M) :