Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

The monoidal closed structure on Module R. #

source
🔸 coverage
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
    Instances For
      source
      🔸 coverage
      instance ModuleCat.instMonoidalClosed {R : Type u} [CommRing R] :
      CategoryTheory.MonoidalClosed (ModuleCat R)
      Equations
        source
        📐 coverage
        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
        📐 coverage
        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
        📐 coverage
        @[simp]
        theorem ModuleCat.monoidalClosed_uncurry {R : Type u} [CommRing R] {M N P : ModuleCat R} (f : N ⟶ M ⟹ P) (x : ↑M) (y : ↑N) :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalClosed.uncurry f)) (x ⊗ₜ[R] y) = (Hom.hom ((CategoryTheory.ConcreteCategory.hom f) y)) x
        source
        📐 coverage
        theorem ModuleCat.ihom_ev_app {R : Type u} [CommRing R] (M N : ModuleCat R) :
        (CategoryTheory.ihom.ev M).app N = ofHom ((TensorProduct.uncurry (RingHom.id R) ↑M ↑(M ⟹ 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
        📐 coverage
        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
        📐 coverage
        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)