Functor categories have chosen finite products #
If C
is a category with chosen finite products, then so is J ⥤ C
.
@[reducible, inline]
abbrev
CategoryTheory.Functor.chosenTerminal
(J : Type u_1)
(C : Type u_2)
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
:
Functor J C
The chosen terminal object in J ⥤ C
.
Equations
Instances For
def
CategoryTheory.Functor.chosenTerminalIsTerminal
(J : Type u_1)
(C : Type u_2)
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
:
The chosen terminal object in J ⥤ C
is terminal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Functor.chosenProd
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
:
Functor J C
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_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.chosenProd_map
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
{X✝ Y✝ : J}
(φ : X✝ ⟶ Y✝)
:
def
CategoryTheory.Functor.chosenProd.fst
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
:
The first projection chosenProd F₁ F₂ ⟶ F₁
.
Equations
- CategoryTheory.Functor.chosenProd.fst F₁ F₂ = { app := fun (x : J) => CategoryTheory.CartesianMonoidalCategory.fst (F₁.obj x) (F₂.obj x), naturality := ⋯ }
Instances For
def
CategoryTheory.Functor.chosenProd.snd
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
:
The second projection chosenProd F₁ F₂ ⟶ F₂
.
Equations
- CategoryTheory.Functor.chosenProd.snd F₁ F₂ = { app := fun (x : J) => CategoryTheory.CartesianMonoidalCategory.snd (F₁.obj x) (F₂.obj x), naturality := ⋯ }
Instances For
def
CategoryTheory.Functor.chosenProd.isLimit
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory 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
instance
CategoryTheory.Functor.cartesianMonoidalCategory
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorObj_obj
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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.{u_5, u_1} J]
[Category.{u_6, 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.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.snd_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ F₂ : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.leftUnitor_hom_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.leftUnitor_inv_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.rightUnitor_hom_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.rightUnitor_inv_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F : Functor J C)
(j : J)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorHom_app_fst
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.fst (F₁'.obj j) (F₂'.obj j)) = CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (f.app j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorHom_app_fst_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
{F₁ F₁' F₂ F₂' : Functor J C}
(f : F₁ ⟶ F₁')
(g : F₂ ⟶ F₂')
(j : J)
{Z : C}
(h : F₁'.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.tensorHom f g).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁'.obj j) (F₂'.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (CategoryStruct.comp (f.app j) h)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorHom_app_snd
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.snd (F₁'.obj j) (F₂'.obj j)) = CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (g.app j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorHom_app_snd_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
{F₁ F₁' F₂ F₂' : Functor J C}
(f : F₁ ⟶ F₁')
(g : F₂ ⟶ F₂')
(j : J)
{Z : C}
(h : F₂'.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.tensorHom f g).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁'.obj j) (F₂'.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (CategoryStruct.comp (g.app j) h)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.fst (F₁.obj j) (F₂'.obj j)) = CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ : Functor J C)
{F₂ F₂' : Functor J C}
(g : F₂ ⟶ F₂')
(j : J)
{Z : C}
(h : F₁.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.whiskerLeft F₁ g).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂'.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.snd (F₁.obj j) (F₂'.obj j)) = CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (g.app j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
(F₁ : Functor J C)
{F₂ F₂' : Functor J C}
(g : F₂ ⟶ F₂')
(j : J)
{Z : C}
(h : F₂'.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.whiskerLeft F₁ g).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂'.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) (CategoryStruct.comp (g.app j) h)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_app_fst
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.fst (F₁'.obj j) (F₂.obj j)) = CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (f.app j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_app_fst_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
{F₁ F₁' : Functor J C}
(f : F₁ ⟶ F₁')
(F₂ : Functor J C)
(j : J)
{Z : C}
(h : F₁'.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.whiskerRight f F₂).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁'.obj j) (F₂.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)) (CategoryStruct.comp (f.app j) h)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_app_snd
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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)
(CartesianMonoidalCategory.snd (F₁'.obj j) (F₂.obj j)) = CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_app_snd_assoc
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, u_2} C]
[CartesianMonoidalCategory C]
{F₁ F₁' : Functor J C}
(f : F₁ ⟶ F₁')
(F₂ : Functor J C)
(j : J)
{Z : C}
(h : F₂.obj j ⟶ Z)
:
CategoryStruct.comp ((MonoidalCategoryStruct.whiskerRight f F₂).app j)
(CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁'.obj j) (F₂.obj j)) h) = CategoryStruct.comp (CartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j)) h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.associator_hom_app
{J : Type u_1}
{C : Type u_2}
[Category.{u_5, u_1} J]
[Category.{u_6, 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.{u_5, u_1} J]
[Category.{u_6, 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.{u_8, u_1} J]
[Category.{u_7, u_2} C]
[CartesianMonoidalCategory C]
{K : Type u_5}
[Category.{u_6, u_5} K]
[Limits.HasColimitsOfShape K C]
[∀ (X : C), Limits.PreservesColimitsOfShape K (MonoidalCategory.tensorLeft X)]
{F : Functor J C}
:
noncomputable def
CategoryTheory.Functor.Monoidal.tensorObjComp
{C : Type u_2}
{D : Type u_3}
{E : Type u_4}
[Category.{u_5, u_2} C]
[Category.{u_6, u_3} D]
[Category.{u_7, 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)) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app
{C : Type u_2}
{D : Type u_3}
{E : Type u_4}
[Category.{u_5, u_2} C]
[Category.{u_6, u_3} D]
[Category.{u_7, u_4} E]
[CartesianMonoidalCategory C]
[CartesianMonoidalCategory E]
(F G : Functor D C)
(H : Functor C E)
[Limits.PreservesFiniteProducts H]
(X : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.tensorObjComp_inv_app
{C : Type u_2}
{D : Type u_3}
{E : Type u_4}
[Category.{u_5, u_2} C]
[Category.{u_6, u_3} D]
[Category.{u_7, 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.{u_5, u_2} C]
[CartesianMonoidalCategory C]
{F G : Functor Cᵒᵖ (Type v)}
{X Y : C}
(h₁ : F.RepresentableBy X)
(h₂ : G.RepresentableBy Y)
:
A tensor product of representable functors is representable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv
{C : Type u_2}
[Category.{u_5, u_2} C]
[CartesianMonoidalCategory C]
{F G : Functor Cᵒᵖ (Type v)}
{X Y : C}
(h₁ : F.RepresentableBy X)
(h₂ : G.RepresentableBy Y)
{I : C}
: