Documentation

Mathlib.CategoryTheory.Monoidal.Types.Basic

The category of types is a (symmetric) monoidal category #

source
@[implicit_reducible]
instance CategoryTheory.typesCartesianMonoidalCategory :
CartesianMonoidalCategory (Type u)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
instance CategoryTheory.instBraidedCategoryType :
BraidedCategory (Type u)
Equations
source
theorem CategoryTheory.types_tensorObj_def {X Y : Type u} :
MonoidalCategoryStruct.tensorObj X Y = (X × Y)
source
theorem CategoryTheory.types_tensorUnit_def :
MonoidalCategoryStruct.tensorUnit (Type u) = PUnit.{u + 1}
source
@[simp]
theorem CategoryTheory.tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : MonoidalCategoryStruct.tensorObj W Y) :
(ConcreteCategory.hom (MonoidalCategoryStruct.tensorHom f g)) p = ((ConcreteCategory.hom f) p.1, (ConcreteCategory.hom g) p.2)
source
@[simp]
theorem CategoryTheory.whiskerLeft_apply (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : MonoidalCategoryStruct.tensorObj X Y) :
(ConcreteCategory.hom (MonoidalCategoryStruct.whiskerLeft X f)) p = (p.1, (ConcreteCategory.hom f) p.2)
source
@[simp]
theorem CategoryTheory.whiskerRight_apply {Y Z : Type u} (f : Y ⟶ Z) (X : Type u) (p : MonoidalCategoryStruct.tensorObj Y X) :
(ConcreteCategory.hom (MonoidalCategoryStruct.whiskerRight f X)) p = ((ConcreteCategory.hom f) p.1, p.2)
source
@[simp]
theorem CategoryTheory.leftUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1}} :
(ConcreteCategory.hom (MonoidalCategoryStruct.leftUnitor X).hom) (p, x) = x
source
@[simp]
theorem CategoryTheory.leftUnitor_inv_apply {X : Type u} {x : X} :
(ConcreteCategory.hom (MonoidalCategoryStruct.leftUnitor X).inv) x = (PUnit.unit, x)
source
@[simp]
theorem CategoryTheory.rightUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1}} :
(ConcreteCategory.hom (MonoidalCategoryStruct.rightUnitor X).hom) (x, p) = x
source
@[simp]
theorem CategoryTheory.rightUnitor_inv_apply {X : Type u} {x : X} :
(ConcreteCategory.hom (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} :
(ConcreteCategory.hom (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} :
(ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z)} :
((ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z)} :
((ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z)} :
((ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))} :
((ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))} :
((ConcreteCategory.hom (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 : (fun (X : Type u) => X) (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z))} :
((ConcreteCategory.hom (MonoidalCategoryStruct.associator X Y Z).inv) x).2 = x.2.2
source
@[simp]
theorem CategoryTheory.braiding_hom_apply {X Y : Type u} {x : X} {y : Y} :
(ConcreteCategory.hom (β_ X Y).hom) (x, y) = (y, x)
source
@[simp]
theorem CategoryTheory.braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
(ConcreteCategory.hom (β_ X Y).inv) (y, x) = (x, y)
source
@[simp]
theorem CategoryTheory.CartesianMonoidalCategory.lift_apply {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X} :
(ConcreteCategory.hom (lift f g)) x = ((ConcreteCategory.hom f) x, (ConcreteCategory.hom g) x)
source
noncomputable def CategoryTheory.MonoidalFunctor.mapPi {C : Type u_1} [Category.{v_1, 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