Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.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 CartesianMonoidalCategory instance.

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

The chosen terminal object in Cat.

Equations
    Instances For
      source
      def CategoryTheory.Cat.chosenTerminalIsTerminal :
      Limits.IsTerminal chosenTerminal

      The chosen terminal object in Cat is terminal.

      Equations
        Instances For
          source
          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
            Instances For
              source
              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
                Instances For
                  source
                  def CategoryTheory.Cat.isLimitProdCone (X Y : Cat) :
                  Limits.IsLimit (X.prodCone Y)

                  The product cone in Cat is indeed a product.

                  Equations
                    Instances For
                      source
                      instance CategoryTheory.Cat.instCartesianMonoidalCategory :
                      CartesianMonoidalCategory Cat
                      Equations
                        source
                        instance CategoryTheory.Cat.instBraidedCategory :
                        BraidedCategory Cat
                        Equations
                          source
                          theorem CategoryTheory.Monoidal.tensorObj (C D : Cat) :
                          MonoidalCategoryStruct.tensorObj C D = Cat.of (↑C × ↑D)
                          source
                          theorem CategoryTheory.Monoidal.whiskerLeft (X : Cat) {A B : Cat} (f : A ⟶ B) :
                          MonoidalCategoryStruct.whiskerLeft X f = (Functor.id ↑X).prod f
                          source
                          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
                          source
                          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
                          source
                          theorem CategoryTheory.Monoidal.whiskerRight {A B : Cat} (f : A ⟶ B) (X : Cat) :
                          MonoidalCategoryStruct.whiskerRight f X = Functor.prod f (Functor.id ↑X)
                          source
                          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
                          source
                          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
                          source
                          theorem CategoryTheory.Monoidal.tensorHom {A B : Cat} (f : A ⟶ B) {X Y : Cat} (g : X ⟶ Y) :
                          MonoidalCategoryStruct.tensorHom f g = Functor.prod f g
                          source
                          theorem CategoryTheory.Monoidal.tensorUnit :
                          MonoidalCategoryStruct.tensorUnit Cat = Cat.chosenTerminal
                          source
                          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))
                          source
                          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))
                          source
                          theorem CategoryTheory.Monoidal.leftUnitor_hom (C : Cat) :
                          (MonoidalCategoryStruct.leftUnitor C).hom = Prod.snd ↑(MonoidalCategoryStruct.tensorUnit Cat) ↑C
                          source
                          theorem CategoryTheory.Monoidal.leftUnitor_inv (C : Cat) :
                          (MonoidalCategoryStruct.leftUnitor C).inv = Prod.sectR { down := { as := PUnit.unit } } ↑C
                          source
                          theorem CategoryTheory.Monoidal.rightUnitor_hom (C : Cat) :
                          (MonoidalCategoryStruct.rightUnitor C).hom = Prod.fst ↑C ↑(MonoidalCategoryStruct.tensorUnit Cat)
                          source
                          theorem CategoryTheory.Monoidal.rightUnitor_inv (C : Cat) :
                          (MonoidalCategoryStruct.rightUnitor C).inv = Prod.sectL ↑C { down := { as := PUnit.unit } }