tensorObjComp

Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.tensorObjComp

Lean4

/-- A finite-products-preserving functor distributes over the tensor product of functors. -/
@[simps!]
noncomputable def tensorObjComp (F G : D ⥤ C) (H : C ⥤ E) [PreservesFiniteProducts H] :
    (F ⊗ G) ⋙ H ≅ (F ⋙ H) ⊗ (G ⋙ H) :=
  NatIso.ofComponents (fun X ↦ prodComparisonIso H (F.obj X) (G.obj X)) fun {X Y} f ↦ by dsimp;
    ext <;> simp [← Functor.map_comp]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru