Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts.Cat

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.

source
@[reducible, inline]
abbrev CategoryTheory.Cat.chosenTerminal :
CategoryTheory.Cat

The chosen terminal object in Cat.

Equations
Instances For
    source
    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.
    Instances For
      source
      def CategoryTheory.Cat.prodCone (C D : CategoryTheory.Cat) :
      CategoryTheory.Limits.BinaryFan C D

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

      Equations
      Instances For
        source
        def CategoryTheory.Cat.isLimitProdCone (X Y : CategoryTheory.Cat) :
        CategoryTheory.Limits.IsLimit (X.prodCone Y)

        The product cone in Cat is indeed a product.

        Equations
        Instances For
          source
          instance CategoryTheory.Cat.instChosenFiniteProducts :
          CategoryTheory.ChosenFiniteProducts CategoryTheory.Cat
          Equations
          • One or more equations did not get rendered due to their size.
          source
          theorem CategoryTheory.Monoidal.tensorObj (C D : CategoryTheory.Cat) :
          CategoryTheory.MonoidalCategory.tensorObj C D = CategoryTheory.Cat.of (↑C × ↑D)
          source
          theorem CategoryTheory.Monoidal.whiskerLeft (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (f : A ⟶ B) :
          CategoryTheory.MonoidalCategory.whiskerLeft X f = (CategoryTheory.Functor.id ↑X).prod f
          source
          theorem CategoryTheory.Monoidal.whiskerLeft_fst (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (f : A ⟶ B) :
          CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (CategoryTheory.Prod.fst ↑X ↑B) = CategoryTheory.Prod.fst ↑X ↑A
          source
          theorem CategoryTheory.Monoidal.whiskerLeft_snd (X : CategoryTheory.Cat) {A 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
          source
          theorem CategoryTheory.Monoidal.whiskerRight {A B : CategoryTheory.Cat} (f : A ⟶ B) (X : CategoryTheory.Cat) :
          CategoryTheory.MonoidalCategory.whiskerRight f X = CategoryTheory.Functor.prod f (CategoryTheory.Functor.id ↑X)
          source
          theorem CategoryTheory.Monoidal.whiskerRight_fst {A 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
          source
          theorem CategoryTheory.Monoidal.whiskerRight_snd {A 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
          source
          theorem CategoryTheory.Monoidal.tensorHom {A B : CategoryTheory.Cat} (f : A ⟶ B) {X Y : CategoryTheory.Cat} (g : X ⟶ Y) :
          CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Functor.prod f g
          source
          theorem CategoryTheory.Monoidal.tensorUnit :
          𝟙_ CategoryTheory.Cat = CategoryTheory.Cat.chosenTerminal
          source
          theorem CategoryTheory.Monoidal.associator_hom (X Y 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))
          source
          theorem CategoryTheory.Monoidal.associator_inv (X Y 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))
          source
          theorem CategoryTheory.Monoidal.leftUnitor_hom (C : CategoryTheory.Cat) :
          (CategoryTheory.MonoidalCategory.leftUnitor C).hom = CategoryTheory.Prod.snd ↑(𝟙_ CategoryTheory.Cat) ↑C
          source
          theorem CategoryTheory.Monoidal.leftUnitor_inv (C : CategoryTheory.Cat) :
          (CategoryTheory.MonoidalCategory.leftUnitor C).inv = CategoryTheory.Prod.sectR { down := { as := PUnit.unit } } ↑C
          source
          theorem CategoryTheory.Monoidal.rightUnitor_hom (C : CategoryTheory.Cat) :
          (CategoryTheory.MonoidalCategory.rightUnitor C).hom = CategoryTheory.Prod.fst ↑C ↑(𝟙_ CategoryTheory.Cat)
          source
          theorem CategoryTheory.Monoidal.rightUnitor_inv (C : CategoryTheory.Cat) :
          (CategoryTheory.MonoidalCategory.rightUnitor C).inv = CategoryTheory.Prod.sectL ↑C { down := { as := PUnit.unit } }