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 ChosenFiniteProducts instance.

@[reducible, inline]

abbrev CategoryTheory.Cat.chosenTerminal : CategoryTheory.Cat

The chosen terminal object in Cat.

Equations

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

def CategoryTheory.Cat.chosenTerminalIsTerminal : CategoryTheory.Limits.IsTerminal CategoryTheory.Cat.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.prodCone (C : CategoryTheory.Cat) (D : CategoryTheory.Cat) : CategoryTheory.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 : CategoryTheory.Cat) (Y : CategoryTheory.Cat) : CategoryTheory.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.instChosenFiniteProducts : CategoryTheory.ChosenFiniteProducts CategoryTheory.Cat

Equations

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Monoidal.tensorUnit : 𝟙_ CategoryTheory.Cat = CategoryTheory.Cat.chosenTerminal

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

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

theorem CategoryTheory.Monoidal.leftUnitor_hom (C : CategoryTheory.Cat) : (CategoryTheory.MonoidalCategory.leftUnitor C).hom = CategoryTheory.Prod.snd ↑(𝟙_ CategoryTheory.Cat) ↑C

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

theorem CategoryTheory.Monoidal.rightUnitor_hom (C : CategoryTheory.Cat) : (CategoryTheory.MonoidalCategory.rightUnitor C).hom = CategoryTheory.Prod.fst ↑C ↑(𝟙_ CategoryTheory.Cat)

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