Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

The monoidal closed structure on Module R. #

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

    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 ModuleCat.ihom_coev_app {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) :
    (CategoryTheory.ihom.coev M).app N = LinearMap.flip (TensorProduct.mk R ↑(Opposite.op M).unop ↑((CategoryTheory.Functor.id (ModuleCat R)).toPrefunctor.obj 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.

    source
    theorem ModuleCat.monoidalClosed_pre_app {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} (P : ModuleCat R) (f : N ⟶ M) :
    (CategoryTheory.MonoidalClosed.pre f).app P = LinearMap.lcomp R (↑P) f