Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

The monoidal closed structure on Module R. #

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
    Equations
    • One or more equations did not get rendered due to their size.
    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))) :
    @[simp]
    theorem ModuleCat.monoidalClosed_uncurry {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {P : ModuleCat R} (f : N (CategoryTheory.ihom M).obj P) (x : M) (y : N) :
    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.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.

    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.