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.

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

Equations
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))) :
@[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) :
@[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) :

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.

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.