Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory

Functor categories have chosen finite products #

If C is a category with chosen finite products, then so is J ⥤ C.

@[reducible, inline]

The chosen terminal object in J ⥤ C.

Equations
Instances For

    The chosen terminal object in J ⥤ C is terminal.

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

      The chosen binary product on J ⥤ C.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.chosenProd_obj {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ F₂ : Functor J C) (j : J) :
        (F₁.chosenProd F₂).obj j = MonoidalCategoryStruct.tensorObj (F₁.obj j) (F₂.obj j)
        @[simp]
        theorem CategoryTheory.Functor.chosenProd_map {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ F₂ : Functor J C) {X✝ Y✝ : J} (φ : X✝ Y✝) :
        (F₁.chosenProd F₂).map φ = MonoidalCategoryStruct.tensorHom (F₁.map φ) (F₂.map φ)

        The first projection chosenProd F₁ F₂ ⟶ F₁.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.chosenProd.fst_app {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ F₂ : Functor J C) (x✝ : J) :
          (fst F₁ F₂).app x✝ = ChosenFiniteProducts.fst (F₁.obj x✝) (F₂.obj x✝)

          The second projection chosenProd F₁ F₂ ⟶ F₂.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.chosenProd.snd_app {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ F₂ : Functor J C) (x✝ : J) :
            (snd F₁ F₂).app x✝ = ChosenFiniteProducts.snd (F₁.obj x✝) (F₂.obj x✝)
            noncomputable def CategoryTheory.Functor.chosenProd.isLimit {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ F₂ : Functor J C) :
            Limits.IsLimit (Limits.BinaryFan.mk (fst F₁ F₂) (snd F₁ F₂))

            Functor.chosenProd F₁ F₂ is a binary product of F₁ and F₂.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.tensorHom_app_fst {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ F₁') (g : F₂ F₂') (j : J) :
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ F₁') (g : F₂ F₂') (j : J) {Z : C} (h : F₁'.obj j Z) :
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.tensorHom_app_snd {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ F₁') (g : F₂ F₂') (j : J) :
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ F₁') (g : F₂ F₂') (j : J) {Z : C} (h : F₂'.obj j Z) :
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ : Functor J C) {F₂ F₂' : Functor J C} (g : F₂ F₂') (j : J) :
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] (F₁ : Functor J C) {F₂ F₂' : Functor J C} (g : F₂ F₂') (j : J) {Z : C} (h : F₁.obj j Z) :
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              @[simp]
              theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [ChosenFiniteProducts C] {F₁ F₁' : Functor J C} (f : F₁ F₁') (F₂ : Functor J C) (j : J) {Z : C} (h : F₂.obj j Z) :
              @[simp]
              @[simp]