Documentation

Mathlib.CategoryTheory.Monoidal.Types.Basic

The category of types is a monoidal category #

source
instance CategoryTheory.typesChosenFiniteProducts :
ChosenFiniteProducts (Type u)
Equations
source
@[simp]
theorem CategoryTheory.tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : MonoidalCategoryStruct.tensorObj W Y) :
MonoidalCategoryStruct.tensorHom f g p = (f p.1, g p.2)
source
@[simp]
theorem CategoryTheory.whiskerLeft_apply (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : MonoidalCategoryStruct.tensorObj X Y) :
MonoidalCategoryStruct.whiskerLeft X f p = (p.1, f p.2)
source
@[simp]
theorem CategoryTheory.whiskerRight_apply {Y Z : Type u} (f : Y ⟶ Z) (X : Type u) (p : MonoidalCategoryStruct.tensorObj Y X) :
MonoidalCategoryStruct.whiskerRight f X p = (f p.1, p.2)
source
@[simp]
theorem CategoryTheory.leftUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1}} :
(MonoidalCategoryStruct.leftUnitor X).hom (p, x) = x
source
@[simp]
theorem CategoryTheory.leftUnitor_inv_apply {X : Type u} {x : X} :
(MonoidalCategoryStruct.leftUnitor X).inv x = (PUnit.unit, x)
source
@[simp]
theorem CategoryTheory.rightUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1}} :
(MonoidalCategoryStruct.rightUnitor X).hom (x, p) = x
source
@[simp]
theorem CategoryTheory.rightUnitor_inv_apply {X : Type u} {x : X} :
(MonoidalCategoryStruct.rightUnitor X).inv x = (x, PUnit.unit)
source
@[simp]
theorem CategoryTheory.associator_hom_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
(MonoidalCategoryStruct.associator X Y Z).hom ((x, y), z) = (x, y, z)
source
@[simp]
theorem CategoryTheory.associator_inv_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
(MonoidalCategoryStruct.associator X Y Z).inv (x, y, z) = ((x, y), z)
source
@[simp]
theorem CategoryTheory.associator_hom_apply_1 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z} :
((MonoidalCategoryStruct.associator X Y Z).hom x).1 = x.1.1
source
@[simp]
theorem CategoryTheory.associator_hom_apply_2_1 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z} :
((MonoidalCategoryStruct.associator X Y Z).hom x).2.1 = x.1.2
source
@[simp]
theorem CategoryTheory.associator_hom_apply_2_2 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z} :
((MonoidalCategoryStruct.associator X Y Z).hom x).2.2 = x.2
source
@[simp]
theorem CategoryTheory.associator_inv_apply_1_1 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)} :
((MonoidalCategoryStruct.associator X Y Z).inv x).1.1 = x.1
source
@[simp]
theorem CategoryTheory.associator_inv_apply_1_2 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)} :
((MonoidalCategoryStruct.associator X Y Z).inv x).1.2 = x.2.1
source
@[simp]
theorem CategoryTheory.associator_inv_apply_2 {X Y Z : Type u} {x : MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)} :
((MonoidalCategoryStruct.associator X Y Z).inv x).2 = x.2.2
source
noncomputable def CategoryTheory.MonoidalFunctor.mapPi {C : Type u_1} [Category.{u_3, u_1} C] [MonoidalCategory C] (F : Functor (Type u_2) C) [F.Monoidal] (n : ℕ) (β : Type u_2) :
F.obj (Fin (n + 1) → β) ≅ MonoidalCategoryStruct.tensorObj (F.obj β) (F.obj (Fin n → β))

If F is a monoidal functor out of Type, it takes the (n+1)st cartesian power of a type to the image of that type, tensored with the image of the nth cartesian power.

Equations
Instances For