noncomputable def
ModuleCat.monoidalClosedHomEquiv
{R : Type u}
[CommRing R]
(M N P : ModuleCat R)
:
((CategoryTheory.MonoidalCategory.tensorLeft M).obj N ⟶ P) ≃ (N ⟶ ((CategoryTheory.linearCoyoneda R (ModuleCat R)).obj (Opposite.op 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.
Equations
- One or more equations did not get rendered due to their size.
theorem
ModuleCat.ihom_map_apply
{R : Type u}
[CommRing R]
{M N P : ModuleCat R}
(f : N ⟶ P)
(g : ↑(ModuleCat.of R (M ⟶ N)))
:
((CategoryTheory.ihom M).map f) g = CategoryTheory.CategoryStruct.comp g f
theorem
ModuleCat.monoidalClosed_curry
{R : Type u}
[CommRing R]
{M N P : ModuleCat R}
(f : CategoryTheory.MonoidalCategory.tensorObj M N ⟶ P)
(x : ↑M)
(y : ↑N)
:
((CategoryTheory.MonoidalClosed.curry f) y) x = f (x ⊗ₜ[R] y)
@[simp]
theorem
ModuleCat.monoidalClosed_uncurry
{R : Type u}
[CommRing R]
{M N P : ModuleCat R}
(f : N ⟶ (CategoryTheory.ihom M).obj P)
(x : ↑M)
(y : ↑N)
:
(CategoryTheory.MonoidalClosed.uncurry f) (x ⊗ₜ[R] y) = (f y) x
theorem
ModuleCat.ihom_ev_app
{R : Type u}
[CommRing R]
(M N : ModuleCat R)
:
(CategoryTheory.ihom.ev M).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}
[CommRing R]
(M N : ModuleCat R)
:
(CategoryTheory.ihom.coev M).app N = (TensorProduct.mk R ↑(Opposite.unop (Opposite.op M)) ↑((CategoryTheory.Functor.id (ModuleCat 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
ModuleCat.monoidalClosed_pre_app
{R : Type u}
[CommRing R]
{M N : ModuleCat R}
(P : ModuleCat R)
(f : N ⟶ M)
:
(CategoryTheory.MonoidalClosed.pre f).app P = LinearMap.lcomp R (↑P) f