Documentation

Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

The currying-uncurrying isomorphism between internal homs of a closed monoidal category #

For a closed monoidal category C, we construct the isomorphism of internal hom objects C(x ⊗ y, z) ≅ C(y, C(x, z)) for any triple of objects x y z : C.

source
def CategoryTheory.MonoidalClosed.ihomCurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
(ihom (MonoidalCategoryStruct.tensorObj x y)).obj z ⟶ (ihom y).obj ((ihom x).obj z)

The currying operation taking a morphism (z ⊗ y) ⟶ x to a morphism y ⟶ C(z, x), constructed as a morphism in C between internal homs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.MonoidalClosed.uncurry_ihomCurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
    uncurry (ihomCurry x y z) = curry (CategoryStruct.comp (MonoidalCategoryStruct.associator x y ((ihom (MonoidalCategoryStruct.tensorObj x y)).obj z)).inv ((ihom.ev (MonoidalCategoryStruct.tensorObj x y)).app z))
    source
    theorem CategoryTheory.MonoidalClosed.uncurry_uncurry_ihomCurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
    uncurry (uncurry (ihomCurry x y z)) = CategoryStruct.comp (MonoidalCategoryStruct.associator x y ((ihom (MonoidalCategoryStruct.tensorObj x y)).obj z)).inv ((ihom.ev (MonoidalCategoryStruct.tensorObj x y)).app z)
    source
    def CategoryTheory.MonoidalClosed.ihomUncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
    (ihom y).obj ((ihom x).obj z) ⟶ (ihom (MonoidalCategoryStruct.tensorObj x y)).obj z

    The uncurrying operation taking a morphism y ⟶ C(x, z) to a morphism (x ⊗ y) ⟶ z, constructed as a morphism in C between internal homs.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.MonoidalClosed.uncurry_ihomUncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
      uncurry (ihomUncurry x y z) = CategoryStruct.comp (MonoidalCategoryStruct.associator x y ((ihom y).obj ((ihom x).obj z))).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft x ((ihom.ev y).app ((ihom x).obj z))) ((ihom.ev x).app z))
      source
      @[simp]
      theorem CategoryTheory.MonoidalClosed.ihomUncurry_ihomCurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
      CategoryStruct.comp (ihomUncurry x y z) (ihomCurry x y z) = CategoryStruct.id ((ihom y).obj ((ihom x).obj z))
      source
      @[simp]
      theorem CategoryTheory.MonoidalClosed.ihomUncurry_ihomCurry_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] {Z : C} (h : (ihom y).obj ((ihom x).obj z) ⟶ Z) :
      CategoryStruct.comp (ihomUncurry x y z) (CategoryStruct.comp (ihomCurry x y z) h) = h
      source
      @[simp]
      theorem CategoryTheory.MonoidalClosed.ihomCurry_ihomUncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
      CategoryStruct.comp (ihomCurry x y z) (ihomUncurry x y z) = CategoryStruct.id ((ihom (MonoidalCategoryStruct.tensorObj x y)).obj z)
      source
      @[simp]
      theorem CategoryTheory.MonoidalClosed.ihomCurry_ihomUncurry_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] {Z : C} (h : (ihom (MonoidalCategoryStruct.tensorObj x y)).obj z ⟶ Z) :
      CategoryStruct.comp (ihomCurry x y z) (CategoryStruct.comp (ihomUncurry x y z) h) = h
      source
      def CategoryTheory.MonoidalClosed.ihomCurryIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
      (ihom (MonoidalCategoryStruct.tensorObj x y)).obj z ≅ (ihom y).obj ((ihom x).obj z)

      The internal currying-uncurrying isomorphism C(x ⊗ y, z) ≅ C(y, C(x, z)).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.MonoidalClosed.ihomCurryIso_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
        (ihomCurryIso x y z).inv = ihomUncurry x y z
        source
        @[simp]
        theorem CategoryTheory.MonoidalClosed.ihomCurryIso_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] [Closed (MonoidalCategoryStruct.tensorObj x y)] :
        (ihomCurryIso x y z).hom = ihomCurry x y z