mathlib3 documentation

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.

source
def Module.monoidal_closed_hom_equiv {R : Type u} [comm_ring R] (M N P : Module R) :
((category_theory.monoidal_category.tensor_left M).obj N ⟶ P) ≃ (N ⟶ ((category_theory.linear_coyoneda R (Module R)).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
source
@[simp]
theorem Module.monoidal_closed_hom_equiv_symm_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : N ⟶ ((category_theory.linear_coyoneda R (Module R)).obj (opposite.op M)).obj P) :
⇑((M.monoidal_closed_hom_equiv N P).symm) f = (β_ M N).hom ≫ tensor_product.lift f
source
@[simp]
theorem Module.monoidal_closed_hom_equiv_apply {R : Type u} [comm_ring R] (M N P : Module R) (f : (category_theory.monoidal_category.tensor_left M).obj N ⟶ P) :
⇑(M.monoidal_closed_hom_equiv N P) f = (tensor_product.mk R ↥N ↥M).compr₂ ((β_ N M).hom ≫ f)
source
@[protected, instance]
def Module.category_theory.monoidal_closed {R : Type u} [comm_ring R] :
category_theory.monoidal_closed (Module R)
Equations
source
theorem Module.ihom_map_apply {R : Type u} [comm_ring R] {M N P : Module R} (f : N ⟶ P) (g : ↥(Module.of R (M ⟶ N))) :
⇑((category_theory.ihom M).map f) g = g ≫ f
source
@[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) :
⇑(⇑(category_theory.monoidal_closed.curry f) y) x = ⇑f (x ⊗ₜ[R] y)
source
@[simp]
theorem Module.monoidal_closed_uncurry {R : Type u} [comm_ring R] {M N P : Module R} (f : N ⟶ (category_theory.ihom M).obj P) (x : ↥M) (y : ↥N) :
⇑(category_theory.monoidal_closed.uncurry f) (x ⊗ₜ[R] y) = ⇑(⇑f y) x
source
theorem Module.ihom_ev_app {R : Type u} [comm_ring R] (M N : Module R) :
(category_theory.ihom.ev M).app N = ⇑(tensor_product.uncurry R ↥M (↥M →ₗ[R] ↥N) ↥N) linear_map.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.

source
theorem Module.ihom_coev_app {R : Type u} [comm_ring R] (M N : Module R) :
(category_theory.ihom.coev M).app N = (tensor_product.mk R ↥(opposite.unop (opposite.op M)) ↥((𝟭 (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.

source
theorem Module.monoidal_closed_pre_app {R : Type u} [comm_ring R] {M N : Module R} (P : Module R) (f : N ⟶ M) :
(category_theory.monoidal_closed.pre f).app P = linear_map.lcomp R ↥P f