hcomp

Mathlib.CategoryTheory.Functor.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.hcomp

Lean4

/-- `hcomp α β` is the horizontal composition of natural transformations. -/
@[simps (attr := grind =)]
def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I where
  app := fun X : C => β.app (F.obj X) ≫ I.map (α.app X)

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

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

Разделы

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

Аффилиация

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