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 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.
Instances For
    source
    noncomputable instance ModuleCat.instMonoidalClosed {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 N P : ModuleCat R} (f : N ⟶ P) (g : ↑(of R (M ⟶ N))) :
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.ihom M).map f)) g = CategoryTheory.CategoryStruct.comp g f
    source
    theorem ModuleCat.monoidalClosed_curry {R : Type u} [CommRing R] {M N P : ModuleCat R} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (x : ↑M) (y : ↑N) :
    (Hom.hom ((Hom.hom (CategoryTheory.MonoidalClosed.curry f)) y)) x = (CategoryTheory.ConcreteCategory.hom f) (x ⊗ₜ[R] y)
    source
    @[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.ConcreteCategory.hom (CategoryTheory.MonoidalClosed.uncurry f)) (x ⊗ₜ[R] y) = (Hom.hom ((CategoryTheory.ConcreteCategory.hom f) y)) x
    source
    theorem ModuleCat.ihom_ev_app {R : Type u} [CommRing R] (M N : ModuleCat R) :
    (CategoryTheory.ihom.ev M).app N = ofHom ((TensorProduct.uncurry R ↑M ↑((CategoryTheory.ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ 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.

    source
    theorem ModuleCat.ihom_coev_app {R : Type u} [CommRing R] (M N : ModuleCat R) :
    (CategoryTheory.ihom.coev M).app N = ofHom₂ (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.

    source
    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 = ofHom (↑homLinearEquiv.symm ∘ₗ LinearMap.lcomp R (↑P) (Hom.hom f) ∘ₗ ↑homLinearEquiv)