Chosen finite products in Cat

This file proves that the cartesian product of a pair of categories agrees with the product in Cat, and provides the associated CartesianMonoidalCategory instance.

@[reducible, inline]

abbrev CategoryTheory.Cat.chosenTerminal : Cat

The chosen terminal object in Cat.

Equations

• CategoryTheory.Cat.chosenTerminal = CategoryTheory.Cat.of (ULift.{?u.2, 0} (CategoryTheory.ULiftHom (CategoryTheory.Discrete Unit)))

def CategoryTheory.Cat.chosenTerminalIsTerminal : Limits.IsTerminal chosenTerminal

The chosen terminal object in Cat is terminal.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Cat.fromChosenTerminalEquiv {C : Type u} [Category.{v, u} C] : Functor (↑chosenTerminal) C ≃ C

The type of functors out of the chosen terminal category is equivalent to the type of objects in the target category. TODO: upgrade to an equivalence of categories.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Cat.prodCone (C D : Cat) : Limits.BinaryFan C D

The chosen product of categories C × D yields a product cone in Cat.

Equations

• C.prodCone D = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Prod.fst ↑C ↑D) (CategoryTheory.Prod.snd ↑C ↑D)

def CategoryTheory.Cat.isLimitProdCone (X Y : Cat) : Limits.IsLimit (X.prodCone Y)

The product cone in Cat is indeed a product.

Equations

• X.isLimitProdCone Y = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (S : CategoryTheory.Limits.BinaryFan X Y) => CategoryTheory.Functor.prod' S.fst S.snd) ⋯ ⋯ ⋯

instance CategoryTheory.Cat.instCartesianMonoidalCategory : CartesianMonoidalCategory Cat

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Cat.instBraidedCategory : BraidedCategory Cat

Equations

• CategoryTheory.Cat.instBraidedCategory = CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory

theorem CategoryTheory.Monoidal.tensorObj (C D : Cat) : MonoidalCategoryStruct.tensorObj C D = Cat.of (↑C × ↑D)

theorem CategoryTheory.Monoidal.whiskerLeft (X : Cat) {A B : Cat} (f : A ⟶ B) : MonoidalCategoryStruct.whiskerLeft X f = (Functor.id ↑X).prod f

theorem CategoryTheory.Monoidal.whiskerLeft_fst (X : Cat) {A B : Cat} (f : A ⟶ B) : Functor.comp (MonoidalCategoryStruct.whiskerLeft X f) (Prod.fst ↑X ↑B) = Prod.fst ↑X ↑A

theorem CategoryTheory.Monoidal.whiskerLeft_snd (X : Cat) {A B : Cat} (f : A ⟶ B) : Functor.comp (MonoidalCategoryStruct.whiskerLeft X f) (Prod.snd ↑X ↑B) = (Prod.snd ↑X ↑A).comp f

theorem CategoryTheory.Monoidal.whiskerRight {A B : Cat} (f : A ⟶ B) (X : Cat) : MonoidalCategoryStruct.whiskerRight f X = Functor.prod f (Functor.id ↑X)

theorem CategoryTheory.Monoidal.whiskerRight_fst {A B : Cat} (f : A ⟶ B) (X : Cat) : Functor.comp (MonoidalCategoryStruct.whiskerRight f X) (Prod.fst ↑B ↑X) = (Prod.fst ↑A ↑X).comp f

theorem CategoryTheory.Monoidal.whiskerRight_snd {A B : Cat} (f : A ⟶ B) (X : Cat) : Functor.comp (MonoidalCategoryStruct.whiskerRight f X) (Prod.snd ↑B ↑X) = Prod.snd ↑A ↑X

theorem CategoryTheory.Monoidal.tensorHom {A B : Cat} (f : A ⟶ B) {X Y : Cat} (g : X ⟶ Y) : MonoidalCategoryStruct.tensorHom f g = Functor.prod f g

theorem CategoryTheory.Monoidal.tensorUnit : MonoidalCategoryStruct.tensorUnit Cat = Cat.chosenTerminal

theorem CategoryTheory.Monoidal.associator_hom (X Y Z : Cat) : (MonoidalCategoryStruct.associator X Y Z).hom = ((Prod.fst (↑X × ↑Y) ↑Z).comp (Prod.fst ↑X ↑Y)).prod' (((Prod.fst (↑X × ↑Y) ↑Z).comp (Prod.snd ↑X ↑Y)).prod' (Prod.snd (↑X × ↑Y) ↑Z))

theorem CategoryTheory.Monoidal.associator_inv (X Y Z : Cat) : (MonoidalCategoryStruct.associator X Y Z).inv = ((Prod.fst (↑X) (↑Y × ↑Z)).prod' ((Prod.snd (↑X) (↑Y × ↑Z)).comp (Prod.fst ↑Y ↑Z))).prod' ((Prod.snd (↑X) (↑Y × ↑Z)).comp (Prod.snd ↑Y ↑Z))

theorem CategoryTheory.Monoidal.leftUnitor_hom (C : Cat) : (MonoidalCategoryStruct.leftUnitor C).hom = Prod.snd ↑(MonoidalCategoryStruct.tensorUnit Cat) ↑C

theorem CategoryTheory.Monoidal.leftUnitor_inv (C : Cat) : (MonoidalCategoryStruct.leftUnitor C).inv = Prod.sectR { down := { as := PUnit.unit } } ↑C

theorem CategoryTheory.Monoidal.rightUnitor_hom (C : Cat) : (MonoidalCategoryStruct.rightUnitor C).hom = Prod.fst ↑C ↑(MonoidalCategoryStruct.tensorUnit Cat)

theorem CategoryTheory.Monoidal.rightUnitor_inv (C : Cat) : (MonoidalCategoryStruct.rightUnitor C).inv = Prod.sectL ↑C { down := { as := PUnit.unit } }