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
🔸 coverage
@[reducible, inline]
abbrev CategoryTheory.Cat.chosenTerminal :
Cat

The chosen terminal object in Cat.

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

    The chosen terminal object in Cat is terminal.

    Instances For
      source
      🔸 coverage
      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.

      Instances For
        source
        🔸 coverage
        def CategoryTheory.Cat.prodCone (C D : Cat) :
        Limits.BinaryFan C D

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

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

          The product cone in Cat is indeed a product.

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