Functor categories have chosen finite products

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

@[inline, reducible]

abbrev CategoryTheory.Functor.chosenTerminal (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] : CategoryTheory.Functor J C

The chosen terminal object in J ⥤ C.

Equations

• CategoryTheory.Functor.chosenTerminal J C = (CategoryTheory.Functor.const J).obj (𝟙_ C)

def CategoryTheory.Functor.chosenTerminalIsTerminal (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Functor.chosenTerminal J C)

The chosen terminal object in J ⥤ C is terminal.

Equations

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

@[simp]

theorem CategoryTheory.Functor.chosenProd_map {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) : ∀ {X Y : J} (φ : X ⟶ Y), (CategoryTheory.Functor.chosenProd F₁ F₂).map φ = CategoryTheory.MonoidalCategory.tensorHom (F₁.map φ) (F₂.map φ)

@[simp]

theorem CategoryTheory.Functor.chosenProd_obj {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Functor.chosenProd F₁ F₂).obj j = CategoryTheory.MonoidalCategory.tensorObj (F₁.obj j) (F₂.obj j)

def CategoryTheory.Functor.chosenProd {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) : CategoryTheory.Functor J C

The chosen binary product on J ⥤ C.

Equations

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

@[simp]

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

def CategoryTheory.Functor.chosenProd.fst {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) : CategoryTheory.Functor.chosenProd F₁ F₂ ⟶ F₁

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

Equations

• CategoryTheory.Functor.chosenProd.fst F₁ F₂ = { app := fun (x : J) => CategoryTheory.ChosenFiniteProducts.fst (F₁.obj x) (F₂.obj x), naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.chosenProd.snd_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Functor.chosenProd.snd F₁ F₂).app j = CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)

def CategoryTheory.Functor.chosenProd.snd {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) : CategoryTheory.Functor.chosenProd F₁ F₂ ⟶ F₂

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

Equations

• CategoryTheory.Functor.chosenProd.snd F₁ F₂ = { app := fun (j : J) => CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j), naturality := ⋯ }

noncomputable def CategoryTheory.Functor.chosenProd.isLimit {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Functor.chosenProd.fst F₁ F₂) (CategoryTheory.Functor.chosenProd.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.

noncomputable instance CategoryTheory.Functor.chosenFiniteProducts (J : Type u_1) (C : Type u_2) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] : CategoryTheory.ChosenFiniteProducts (CategoryTheory.Functor J C)

Equations

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

@[simp]

theorem CategoryTheory.Functor.Monoidal.leftUnitor_hom_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.leftUnitor F).hom.app j = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj j)).hom

@[simp]

theorem CategoryTheory.Functor.Monoidal.leftUnitor_inv_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.leftUnitor F).inv.app j = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj j)).inv

@[simp]

theorem CategoryTheory.Functor.Monoidal.rightUnitor_hom_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.rightUnitor F).hom.app j = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj j)).hom

@[simp]

theorem CategoryTheory.Functor.Monoidal.rightUnitor_inv_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.rightUnitor F).inv.app j = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj j)).inv

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) {Z : C} (h : F₁'.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂'.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (CategoryTheory.CategoryStruct.comp (f.app j) h)

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_fst {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (f.app j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) {Z : C} (h : F₂'.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂'.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (CategoryTheory.CategoryStruct.comp (g.app j) h)

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_snd {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (g.app j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J) {Z : C} (h : F₁.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂'.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂'.obj j)) = CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J) {Z : C} (h : F₂'.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂'.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (CategoryTheory.CategoryStruct.comp (g.app j) h)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) {F₂ : CategoryTheory.Functor J C} {F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (g.app j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_fst_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J) {Z : C} (h : F₁'.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (CategoryTheory.CategoryStruct.comp (f.app j) h)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_fst {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (f.app j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J) {Z : C} (h : F₂.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂.obj j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_snd {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] {F₁ : CategoryTheory.Functor J C} {F₁' : CategoryTheory.Functor J C} (f : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor J C) (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂.obj j)) = CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.associator_hom_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) (F₃ : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.associator F₁ F₂ F₃).hom.app j = (CategoryTheory.MonoidalCategory.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom

@[simp]

theorem CategoryTheory.Functor.Monoidal.associator_inv_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.ChosenFiniteProducts C] (F₁ : CategoryTheory.Functor J C) (F₂ : CategoryTheory.Functor J C) (F₃ : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.MonoidalCategory.associator F₁ F₂ F₃).inv.app j = (CategoryTheory.MonoidalCategory.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv