The cartesian monoidal structure on type-valued functors, elementwise #
For functors F G : J ⥤ Type v, the product functor F ⊗ G takes the value F.obj j × G.obj j
at j. This file records how its action on morphisms, the whiskering F ◁ g and the projections
fst F G and snd F G act on elements, together with the pointwise braiding and associator.
Mathlib's Functor.Monoidal.tensorObj_map and tensor_apply do not compose to give the
elementwise map equation, as the types of the two sides of the former differ syntactically.
theorem
CategoryTheory.Functor.Monoidal.tensorObj_map_apply
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G : Functor J (Type v)}
{j j' : J}
(f : j ⟶ j')
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
(ConcreteCategory.hom ((MonoidalCategoryStruct.tensorObj F G).map f)) x = ((ConcreteCategory.hom (F.map f)) x.1, (ConcreteCategory.hom (G.map f)) x.2)
theorem
CategoryTheory.Functor.Monoidal.tensorObj_map_apply_fst
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G : Functor J (Type v)}
{j j' : J}
(f : j ⟶ j')
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
((ConcreteCategory.hom ((MonoidalCategoryStruct.tensorObj F G).map f)) x).1 = (ConcreteCategory.hom (F.map f)) x.1
theorem
CategoryTheory.Functor.Monoidal.tensorObj_map_apply_snd
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G : Functor J (Type v)}
{j j' : J}
(f : j ⟶ j')
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
((ConcreteCategory.hom ((MonoidalCategoryStruct.tensorObj F G).map f)) x).2 = (ConcreteCategory.hom (G.map f)) x.2
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_apply_fst
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G G' : Functor J (Type v)}
(g : G ⟶ G')
{j : J}
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_app_apply_snd
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G G' : Functor J (Type v)}
(g : G ⟶ G')
{j : J}
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
((ConcreteCategory.hom ((MonoidalCategoryStruct.whiskerLeft F g).app j)) x).2 = (ConcreteCategory.hom (g.app j)) x.2
theorem
CategoryTheory.Functor.Monoidal.fst_app_apply
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G : Functor J (Type v)}
{j : J}
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
theorem
CategoryTheory.Functor.Monoidal.snd_app_apply
{J : Type u_1}
[Category.{v_1, u_1} J]
{F G : Functor J (Type v)}
{j : J}
(x : (MonoidalCategoryStruct.tensorObj F G).obj j)
:
theorem
TauCeti.braiding_hom_app_apply
{J : Type u_1}
[CategoryTheory.Category.{v_1, u_1} J]
{F G : CategoryTheory.Functor J (Type v)}
{j : J}
{x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj j}
:
The pointwise braiding interchanges the two components of a pair.
theorem
TauCeti.associator_hom_app_apply
{J : Type u_1}
[CategoryTheory.Category.{v_1, u_1} J]
{F G H : CategoryTheory.Functor J (Type v)}
{j : J}
{x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) H).obj j}
:
(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.associator F G H).hom.app j)) x = (x.1.1, x.1.2, x.2)
The pointwise associator regroups a left-associated triple.
theorem
TauCeti.associator_inv_app_apply
{J : Type u_1}
[CategoryTheory.Category.{v_1, u_1} J]
{F G H : CategoryTheory.Functor J (Type v)}
{j : J}
{x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)).obj j}
:
The inverse pointwise associator regroups a right-associated triple.
theorem
TauCeti.whiskerLeft_app_apply
{J : Type u_1}
[CategoryTheory.Category.{v_1, u_1} J]
{F G : CategoryTheory.Functor J (Type v)}
{j : J}
{G' : CategoryTheory.Functor J (Type v)}
{g : G ⟶ G'}
{x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj j}
:
(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g).app j)) x = (x.1, (CategoryTheory.ConcreteCategory.hom (g.app j)) x.2)
Left whiskering keeps the first component and applies the natural transformation to the second component.