CategoryTheory.MonoidalClosed.pre_id
theorem CategoryTheory.MonoidalClosed.pre_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
[inst_2 : CategoryTheory.Closed A],
CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.id A) =
CategoryTheory.CategoryStruct.id (CategoryTheory.ihom A)
This theorem, `CategoryTheory.MonoidalClosed.pre_id`, states that for any object `A` in a monoidal category `C` that is also a closed category, applying the `pre` functor to the identity morphism on `A` is the same as the identity morphism on the internal hom functor (`ihom`) applied to `A`. In other words, in the context of category theory, it asserts the identity law for the `pre` functor with respect to the identity morphism, which is important in studying how functors behave with identity morphisms.
More concisely: In a monoidal and closed category, the `pre` functor applied to the identity morphism of an object is equal to the identity morphism of the internal hom functor applied to that object.
|
CategoryTheory.ihom.coev_ev
theorem CategoryTheory.ihom.coev_ev :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
[inst_2 : CategoryTheory.Closed A],
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B))
((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) =
CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj B)
The theorem `CategoryTheory.ihom.coev_ev` states that for any type C, in the context of a category structure and a monoidal category, and for any two objects A and B in C such that A is a closed object, the composition of the application of the coevaluation natural transformation on the object B transformed by the internal hom functor with the map of the application of the evaluation natural transformation on B through the internal hom functor, equals the identity morphism on the object B transformed by the internal hom functor. This is a property of internal hom functors in a monoidal category with a specified closed object.
More concisely: For any object B in a monoidal category with a closed object A, the composition of the coevaluation and evaluation morphisms through the internal hom functor equals the identity morphism on B.
|
CategoryTheory.ihom.ev_coev
theorem CategoryTheory.ihom.ev_coev :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A B : C)
[inst_2 : CategoryTheory.Closed A],
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom.coev A).app B))
((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategory.tensorObj A B)) =
CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A B)
The theorem `CategoryTheory.ihom.ev_coev` states that for any category `C` that is also a monoidal category, and for any objects `A` and `B` in `C` where `A` is a closed object, the composition of the coevaluation natural transformation (which is whiskered left by `A`) applied to `B` and the evaluation natural transformation applied to the tensor product of `A` and `B` is equivalent to the identity morphism on the tensor product of `A` and `B`. In other words, the coevaluation and evaluation natural transformations satisfy a certain kind of "round trip" property in the context of monoidal categories.
More concisely: For any monoidal category `C` and objects `A, B` in `C` with `A` closed, the coevaluation and evaluation natural transformations satisfy `coev(B) ∘ ev(A ⊗ B) ≈ id(A ⊗ B)`.
|
CategoryTheory.MonoidalClosed.ofEquiv_curry_def
theorem 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.MonoidalFunctor C D) [inst_4 : F.IsEquivalence] [inst_5 : CategoryTheory.MonoidalClosed D]
{X Y Z : C} (f : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z),
CategoryTheory.MonoidalClosed.curry f =
(F.adjunction.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.inv.inv.obj Z)))
(CategoryTheory.MonoidalClosed.curry
((F.inv.adjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)) Z)
(CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInvIso.hom.app Y) f)))
This theorem establishes a relationship between the currying operation in two monoidal categories that are equivalent. Suppose we have a monoidal equivalence `F : C ≌ D`, where `D` is a monoidal closed category. This theorem states that we can pull back the monoidal closed structure along the equivalence to `C`. For any three objects `X, Y, Z : C`, the theorem defines the currying map from the hom-set `Hom(X ⊗ Y, Z)` to `Hom(Y, (X ⟶[C] Z))` in `C`, in terms of currying in `D` and the equivalence `F`. In particular, `X ⟶[C] Z` is defined to be `F⁻¹(F(X) ⟶[D] F(Z))`, meaning that currying in `C` essentially conjugates currying in `D` by `F`.
More concisely: Given a monoidal equivalence `F : C ≌ D` in a monoidal closed category `D`, the currying operation in `C` is defined as the pullback of currying in `D` along `F`.
|
CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def
theorem CategoryTheory.MonoidalClosed.ofEquiv_uncurry_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.MonoidalFunctor C D) [inst_4 : F.IsEquivalence] [inst_5 : CategoryTheory.MonoidalClosed D]
{X Y Z : C} (f : Y ⟶ (CategoryTheory.ihom X).obj Z),
CategoryTheory.MonoidalClosed.uncurry f =
CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInvIso.inv.app Y)
((F.inv.adjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)) Z).symm
(CategoryTheory.MonoidalClosed.uncurry
((F.adjunction.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.obj Z))).symm f)))
This theorem addresses a scenario where we have a monoidal equivalence `F` between categories `C` and `D`, where `D` is monoidally closed. It then shows how to pull back the monoidal closed instance from `D` to `C`. Given `X, Y, Z` objects in `C`, the theorem describes an uncurrying map from the space of morphisms from `Y` to the internal hom-object `(X ⟶[C] Z)` to the space of morphisms from the tensor product of `X` and `Y` to `Z`. Here, the internal hom-object `(X ⟶[C] Z)` is defined as the inverse image under `F` of the morphisms from `F(X)` to `F(Z)` in `D`. The uncurrying in `C` is essentially achieved by conjugating the uncurrying in `D` by `F`.
More concisely: Given a monoidal equivalence `F` from category `C` to monoidally closed category `D`, the theorem provides an isomorphism between the space of morphisms from `Y` to the internal hom-object `(X ⟶[C] Z)` in `C` and the space of morphisms from `X ⊗ Y` to `Z` in `C`, where the internal hom-object is defined as the inverse image under `F` of morphisms from `F(X)` to `F(Z)` in `D`.
|