Functor categories have chosen finite products

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

@[implicit_reducible]

instance CategoryTheory.Functor.cartesianMonoidalCategory {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] : CartesianMonoidalCategory (Functor J C)

Equations

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

@[deprecated CategoryTheory.MonoidalCategoryStruct.tensorUnit (since := "2026-03-07")]

def CategoryTheory.Functor.chosenTerminal (C : Type u) {𝒞 : Category.{v, u} C} [self : MonoidalCategoryStruct C] : C

Alias of CategoryTheory.MonoidalCategoryStruct.tensorUnit.

Equations

• CategoryTheory.Functor.chosenTerminal = CategoryTheory.MonoidalCategoryStruct.tensorUnit

@[deprecated CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit (since := "2026-03-07")]

def CategoryTheory.Functor.chosenTerminalIsTerminal {C : Type u} {inst✝ : Category.{v, u} C} [self : SemiCartesianMonoidalCategory C] : Limits.IsTerminal (MonoidalCategoryStruct.tensorUnit C)

Alias of CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.

Equations

• @CategoryTheory.Functor.chosenTerminalIsTerminal = @CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit

@[deprecated CategoryTheory.MonoidalCategoryStruct.tensorObj (since := "2026-03-07")]

def CategoryTheory.Functor.chosenProd {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategoryStruct C] : C → C → C

Alias of CategoryTheory.MonoidalCategoryStruct.tensorObj.

Equations

• @CategoryTheory.Functor.chosenProd = @CategoryTheory.MonoidalCategoryStruct.tensorObj

@[deprecated CategoryTheory.SemiCartesianMonoidalCategory.fst (since := "2026-03-07")]

def CategoryTheory.Functor.chosenProd.fst {C : Type u} {inst✝ : Category.{v, u} C} [self : SemiCartesianMonoidalCategory C] (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ X

Alias of CategoryTheory.SemiCartesianMonoidalCategory.fst.

Equations

• @CategoryTheory.Functor.chosenProd.fst = @CategoryTheory.SemiCartesianMonoidalCategory.fst

@[deprecated CategoryTheory.SemiCartesianMonoidalCategory.snd (since := "2026-03-07")]

def CategoryTheory.Functor.chosenProd.snd {C : Type u} {inst✝ : Category.{v, u} C} [self : SemiCartesianMonoidalCategory C] (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ Y

Alias of CategoryTheory.SemiCartesianMonoidalCategory.snd.

Equations

• @CategoryTheory.Functor.chosenProd.snd = @CategoryTheory.SemiCartesianMonoidalCategory.snd

@[deprecated CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct (since := "2026-03-07")]

def CategoryTheory.Functor.chosenProd.isLimit {C : Type u} {inst✝ : Category.{v, u} C} [self : CartesianMonoidalCategory C] (X Y : C) : Limits.IsLimit (Limits.BinaryFan.mk (SemiCartesianMonoidalCategory.fst X Y) (SemiCartesianMonoidalCategory.snd X Y))

Alias of CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct.

Equations

• @CategoryTheory.Functor.chosenProd.isLimit = @CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorObj_obj {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ : Functor J C) (j : J) : (MonoidalCategoryStruct.tensorObj F₁ F₂).obj j = MonoidalCategoryStruct.tensorObj (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorObj_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ : Functor J C) {j j' : J} (f : j ⟶ j') : (MonoidalCategoryStruct.tensorObj F₁ F₂).map f = MonoidalCategoryStruct.tensorHom (F₁.map f) (F₂.map f)

@[simp]

theorem CategoryTheory.Functor.Monoidal.fst_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ : Functor J C) (j : J) : (SemiCartesianMonoidalCategory.fst F₁ F₂).app j = SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.snd_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ : Functor J C) (j : J) : (SemiCartesianMonoidalCategory.snd F₁ F₂).app j = SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.leftUnitor_hom_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F : Functor J C) (j : J) : (MonoidalCategoryStruct.leftUnitor F).hom.app j = (MonoidalCategoryStruct.leftUnitor (F.obj j)).hom

@[simp]

theorem CategoryTheory.Functor.Monoidal.leftUnitor_inv_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F : Functor J C) (j : J) : (MonoidalCategoryStruct.leftUnitor F).inv.app j = (MonoidalCategoryStruct.leftUnitor (F.obj j)).inv

@[simp]

theorem CategoryTheory.Functor.Monoidal.rightUnitor_hom_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F : Functor J C) (j : J) : (MonoidalCategoryStruct.rightUnitor F).hom.app j = (MonoidalCategoryStruct.rightUnitor (F.obj j)).hom

@[simp]

theorem CategoryTheory.Functor.Monoidal.rightUnitor_inv_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F : Functor J C) (j : J) : (MonoidalCategoryStruct.rightUnitor F).inv.app j = (MonoidalCategoryStruct.rightUnitor (F.obj j)).inv

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_fst {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.tensorHom f g).app j) (SemiCartesianMonoidalCategory.fst (F₁'.obj j) (F₂'.obj j)) = CategoryStruct.comp (SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (f.app j)

theorem CategoryTheory.Functor.Monoidal.tensorHom_app_snd {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F₁ F₁' F₂ F₂' : Functor J C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.tensorHom f g).app j) (SemiCartesianMonoidalCategory.snd (F₁'.obj j) (F₂'.obj j)) = CategoryStruct.comp (SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (g.app j)

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ : Functor J C) {F₂ F₂' : Functor J C} (g : F₂ ⟶ F₂') (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.whiskerLeft F₁ g).app j) (SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂'.obj j)) = SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)

theorem CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ : Functor J C) {F₂ F₂' : Functor J C} (g : F₂ ⟶ F₂') (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.whiskerLeft F₁ g).app j) (SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂'.obj j)) = CategoryStruct.comp (SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (g.app j)

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_fst {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F₁ F₁' : Functor J C} (f : F₁ ⟶ F₁') (F₂ : Functor J C) (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.whiskerRight f F₂).app j) (SemiCartesianMonoidalCategory.fst (F₁'.obj j) (F₂.obj j)) = CategoryStruct.comp (SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (f.app j)

theorem CategoryTheory.Functor.Monoidal.whiskerRight_app_snd {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F₁ F₁' : Functor J C} (f : F₁ ⟶ F₁') (F₂ : Functor J C) (j : J) : CategoryStruct.comp ((MonoidalCategoryStruct.whiskerRight f F₂).app j) (SemiCartesianMonoidalCategory.snd (F₁'.obj j) (F₂.obj j)) = SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)

@[simp]

theorem CategoryTheory.Functor.Monoidal.associator_hom_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ F₃ : Functor J C) (j : J) : (MonoidalCategoryStruct.associator F₁ F₂ F₃).hom.app j = (MonoidalCategoryStruct.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} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] (F₁ F₂ F₃ : Functor J C) (j : J) : (MonoidalCategoryStruct.associator F₁ F₂ F₃).inv.app j = (MonoidalCategoryStruct.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv

instance CategoryTheory.Functor.Monoidal.instPreservesColimitsOfShapeTensorLeftOfHasColimitsOfShape {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {K : Type u_5} [Category.{v_5, u_5} K] [Limits.HasColimitsOfShape K C] [∀ (X : C), Limits.PreservesColimitsOfShape K (MonoidalCategory.tensorLeft X)] {F : Functor J C} : Limits.PreservesColimitsOfShape K (MonoidalCategory.tensorLeft F)

noncomputable def CategoryTheory.Functor.Monoidal.tensorObjComp {C : Type u_2} {D : Type u_3} {E : Type u_4} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] [Category.{v_4, u_4} E] [CartesianMonoidalCategory C] [CartesianMonoidalCategory E] (F G : Functor D C) (H : Functor C E) [Limits.PreservesFiniteProducts H] : (MonoidalCategoryStruct.tensorObj F G).comp H ≅ MonoidalCategoryStruct.tensorObj (F.comp H) (G.comp H)

A finite-products-preserving functor distributes over the tensor product of functors.

Equations

• CategoryTheory.Functor.Monoidal.tensorObjComp F G H = CategoryTheory.NatIso.ofComponents (fun (X : D) => CategoryTheory.CartesianMonoidalCategory.prodComparisonIso H (F.obj X) (G.obj X)) ⋯

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app {C : Type u_2} {D : Type u_3} {E : Type u_4} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] [Category.{v_4, u_4} E] [CartesianMonoidalCategory C] [CartesianMonoidalCategory E] (F G : Functor D C) (H : Functor C E) [Limits.PreservesFiniteProducts H] (X : D) : (tensorObjComp F G H).hom.app X = CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X)

@[simp]

theorem CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app {C : Type u_2} {D : Type u_3} {E : Type u_4} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] [Category.{v_4, u_4} E] [CartesianMonoidalCategory C] [CartesianMonoidalCategory E] (F G : Functor D C) (H : Functor C E) [Limits.PreservesFiniteProducts H] (X : D) : (tensorObjComp F G H).inv.app X = (CartesianMonoidalCategory.prodComparisonIso H (F.obj X) (G.obj X)).inv

def CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj {C : Type u_2} [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F G : Functor Cᵒᵖ (Type v)} {X Y : C} (h₁ : F.RepresentableBy X) (h₂ : G.RepresentableBy Y) : (MonoidalCategoryStruct.tensorObj F G).RepresentableBy (MonoidalCategoryStruct.tensorObj X Y)

A tensor product of representable functors is representable.

Equations

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

@[simp]

theorem CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv {C : Type u_2} [Category.{v_2, u_2} C] [CartesianMonoidalCategory C] {F G : Functor Cᵒᵖ (Type v)} {X Y : C} (h₁ : F.RepresentableBy X) (h₂ : G.RepresentableBy Y) {I : C} : (RepresentableBy.tensorObj h₁ h₂).homEquiv = CartesianMonoidalCategory.homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)