Documentation

TauCeti.CategoryTheory.Monoidal.Mod.Closed

Closedness of the balanced tensor product #

For a commutative monoid object A in a braided closed monoidal category, the internal object of A-linear maps is right adjoint to balanced tensoring with a module. Thus the balanced tensor product and Mod.internalHom make Mod C A monoidal closed, provided that equalizers and tensor-preserved coequalizers exist.

The bijection is ordinary currying on representatives. Linearity in the first variable makes a curried map land in the equalizer of linear maps; balancing is exactly linearity of that map in the second variable. In particular this identifies function spectra with the internal hom for the point-set smash product, without any model-category assertion.

References #

source
theorem CategoryTheory.Mod.isModHom_ihomHomEquiv_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] (M K N : Mod C A) (f : M.tensorLeft.obj K.X ⟶ N) :
IsModHom A ((M.ihomHomEquiv K.X N) f) ↔ CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) K.X) f.hom = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A K.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f.hom)

Currying a map linear in its first variable gives a module map exactly when the original map is balanced in its two variables.

source
noncomputable def CategoryTheory.Mod.tensorHomEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) :
(MonoidalCategoryStruct.tensorObj M K ⟶ N) ≃ (K ⟶ M.internalHom.obj N)

Balanced tensoring with M is left adjoint to the module of linear maps out of M: the bijection is currying after precomposing with the balanced quotient.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Mod.tensorHomEquiv_apply_hom_comp_ihomι {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) (f : MonoidalCategoryStruct.tensorObj M K ⟶ N) :
    CategoryStruct.comp ((M.tensorHomEquiv K N) f).hom (M.ihomι N) = MonoidalClosed.curry (CategoryStruct.comp (M.tensorπ K) f.hom)

    The curried module map, included into the ambient internal hom, is ordinary currying of the map on representatives.

    source
    @[simp]
    theorem CategoryTheory.Mod.tensorHomEquiv_apply_hom_comp_ihomι_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) (f : MonoidalCategoryStruct.tensorObj M K ⟶ N) {Z : C} (h : (CategoryTheory.ihom M.X).obj N.X ⟶ Z) :
    CategoryStruct.comp ((M.tensorHomEquiv K N) f).hom (CategoryStruct.comp (M.ihomι N) h) = CategoryStruct.comp (MonoidalClosed.curry (CategoryStruct.comp (M.tensorπ K) f.hom)) h

    The curried module map, included into the ambient internal hom, is ordinary currying of the map on representatives.

    source
    @[simp]
    theorem CategoryTheory.Mod.tensorπ_tensorHomEquiv_symm_apply_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) (g : K ⟶ M.internalHom.obj N) :
    CategoryStruct.comp (M.tensorπ K) ((M.tensorHomEquiv K N).symm g).hom = MonoidalClosed.uncurry (CategoryStruct.comp g.hom (M.ihomι N))

    Uncurrying a module map evaluates it on representatives of the balanced tensor.

    source
    @[simp]
    theorem CategoryTheory.Mod.tensorπ_tensorHomEquiv_symm_apply_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) (g : K ⟶ M.internalHom.obj N) {Z : C} (h : N.X ⟶ Z) :
    CategoryStruct.comp (M.tensorπ K) (CategoryStruct.comp ((M.tensorHomEquiv K N).symm g).hom h) = CategoryStruct.comp (MonoidalClosed.uncurry (CategoryStruct.comp g.hom (M.ihomι N))) h

    Uncurrying a module map evaluates it on representatives of the balanced tensor.

    source
    noncomputable def CategoryTheory.Mod.internalHomAdjunction {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M : Mod C A) :
    MonoidalCategory.tensorLeft M ⊣ M.internalHom

    The balanced tensor product is left adjoint to the internal module of linear maps.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Mod.internalHomAdjunction_homEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M : Mod C A) :
      M.internalHomAdjunction.homEquiv = M.tensorHomEquiv

      The hom-set bijection of the balanced tensor adjunction is currying on representatives.

      source
      @[instance_reducible]
      noncomputable instance CategoryTheory.Mod.monoidalClosed {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] :
      MonoidalClosed (Mod C A)

      Modules over a commutative monoid in a braided closed monoidal category form a closed monoidal category under balanced tensor, with the equalizer internal hom.

      source
      theorem CategoryTheory.Mod.curry_eq_tensorHomEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M K N : Mod C A) (f : MonoidalCategoryStruct.tensorObj M K ⟶ N) :
      MonoidalClosed.curry f = (M.tensorHomEquiv K N) f

      Native currying for the closed module category is the balanced tensor bijection.

      source
      @[simp]
      theorem CategoryTheory.Mod.tensorπ_ihom_ev_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M N : Mod C A) :
      CategoryStruct.comp (M.tensorπ (M.internalHom.obj N)) ((ihom.ev M).app N).hom = MonoidalClosed.uncurry (M.ihomι N)

      Evaluation for the closed module category is evaluation of linear maps on representatives of the balanced tensor.

      source
      @[simp]
      theorem CategoryTheory.Mod.tensorπ_ihom_ev_app_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] (M N : Mod C A) {Z : C} (h : N.X ⟶ Z) :
      CategoryStruct.comp (CategoryStruct.comp (M.tensorπ { X := M.ihom.obj N, mod := M.ihomModObj N }) ((ihom.ev M).app N).hom) h = CategoryStruct.comp (MonoidalClosed.uncurry (M.ihomι N)) h

      Evaluation for the closed module category is evaluation of linear maps on representatives of the balanced tensor.

      source
      theorem CategoryTheory.Mod.pre_app_hom_comp_ihomι {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {M M' : Mod C A} (f : M ⟶ M') (N : Mod C A) :
      CategoryStruct.comp ((MonoidalClosed.pre f).app N).hom (M.ihomι N) = CategoryStruct.comp (M'.ihomι N) ((MonoidalClosed.pre f.hom).app N.X)

      Precomposition of internal module maps is ambient precomposition after inclusion.

      source
      theorem CategoryTheory.Mod.pre_app_hom_comp_ihomι_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [MonoidalClosed C] [Limits.HasEqualizers C] {A : C} [MonObj A] [IsCommMonObj A] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {M M' : Mod C A} (f : M ⟶ M') (N : Mod C A) {Z : C} (h : (CategoryTheory.ihom M.X).obj N.X ⟶ Z) :
      CategoryStruct.comp (CategoryStruct.comp ((MonoidalClosed.pre f).app N).hom (M.ihomι N)) h = CategoryStruct.comp (CategoryStruct.comp (M'.ihomι N) ((MonoidalClosed.pre f.hom).app N.X)) h

      Precomposition of internal module maps is ambient precomposition after inclusion.