The category of types is a monoidal category #
@[simp]
theorem
CategoryTheory.tensor_apply
{W : Type u}
{X : Type u}
{Y : Type u}
{Z : Type u}
(f : W ⟶ X)
(g : Y ⟶ Z)
(p : CategoryTheory.MonoidalCategory.tensorObj W Y)
:
CategoryTheory.MonoidalCategory.tensorHom f g p = (f p.1, g p.2)
@[simp]
theorem
CategoryTheory.whiskerLeft_apply
(X : Type u)
{Y : Type u}
{Z : Type u}
(f : Y ⟶ Z)
(p : CategoryTheory.MonoidalCategory.tensorObj X Y)
:
CategoryTheory.MonoidalCategory.whiskerLeft X f p = (p.1, f p.2)
@[simp]
theorem
CategoryTheory.whiskerRight_apply
{Y : Type u}
{Z : Type u}
(f : Y ⟶ Z)
(X : Type u)
(p : CategoryTheory.MonoidalCategory.tensorObj Y X)
:
CategoryTheory.MonoidalCategory.whiskerRight f X p = (f p.1, p.2)
@[simp]
theorem
CategoryTheory.leftUnitor_hom_apply
{X : Type u}
{x : X}
{p : PUnit.{u + 1} }
:
(CategoryTheory.MonoidalCategory.leftUnitor X).hom (p, x) = x
@[simp]
theorem
CategoryTheory.leftUnitor_inv_apply
{X : Type u}
{x : X}
:
(CategoryTheory.MonoidalCategory.leftUnitor X).inv x = (PUnit.unit, x)
@[simp]
theorem
CategoryTheory.rightUnitor_hom_apply
{X : Type u}
{x : X}
{p : PUnit.{u + 1} }
:
(CategoryTheory.MonoidalCategory.rightUnitor X).hom (x, p) = x
@[simp]
theorem
CategoryTheory.rightUnitor_inv_apply
{X : Type u}
{x : X}
:
(CategoryTheory.MonoidalCategory.rightUnitor X).inv x = (x, PUnit.unit)
@[simp]
theorem
CategoryTheory.associator_hom_apply
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : X}
{y : Y}
{z : Z}
:
(CategoryTheory.MonoidalCategory.associator X Y Z).hom ((x, y), z) = (x, y, z)
@[simp]
theorem
CategoryTheory.associator_inv_apply
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : X}
{y : Y}
{z : Z}
:
(CategoryTheory.MonoidalCategory.associator X Y Z).inv (x, y, z) = ((x, y), z)
@[simp]
theorem
CategoryTheory.associator_hom_apply_1
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).hom x).1 = x.1.1
@[simp]
theorem
CategoryTheory.associator_hom_apply_2_1
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).hom x).2.1 = x.1.2
@[simp]
theorem
CategoryTheory.associator_hom_apply_2_2
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).hom x).2.2 = x.2
@[simp]
theorem
CategoryTheory.associator_inv_apply_1_1
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).inv x).1.1 = x.1
@[simp]
theorem
CategoryTheory.associator_inv_apply_1_2
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).inv x).1.2 = x.2.1
@[simp]
theorem
CategoryTheory.associator_inv_apply_2
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)}
:
((CategoryTheory.MonoidalCategory.associator X Y Z).inv x).2 = x.2.2
noncomputable def
CategoryTheory.MonoidalFunctor.mapPi
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.MonoidalFunctor (Type u_2) C)
(n : ℕ)
(β : Type u_2)
:
F.obj (Fin (n + 1) → β) ≅ CategoryTheory.MonoidalCategory.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
- F.mapPi n β = F.mapIso (Fin.consEquiv fun (a : Fin (n + 1)) => β).symm.toIso ≪≫ (CategoryTheory.asIso (F.μ β (Fin n → β))).symm