Theorems · Theorem · category theory

CategoryTheory.MonoidalClosed.ofEquiv_curry_def

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : F.IsEquivalence] [inst_6 : CategoryTheory.MonoidalClosed D] {X Y Z : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.MonoidalClosed.curry f =
    (adj.homEquiv Y (F.obj X ⟹ F.obj Z))
      (CategoryTheory.MonoidalClosed.curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z)
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y) f)))

Suppose we have a monoidal equivalence F : C ≌ D, with D monoidal closed. We can pull the monoidal closed instance back along the equivalence. For X, Y, Z : C, this lemma describes the resulting currying map Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z)). (X ⟶[C] Z is defined to be F⁻¹(F(X) ⟶[D] F(Z)), so currying in C is given by essentially conjugating currying in D by F.)

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Basic

Cited by

0 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.MonoidalCategoryTheory.Functor.IsEquivalenceCategoryTheory.MonoidalClosed