comp

Mathlib.CategoryTheory.Functor.FunctorHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.HomObj.comp

Lean4

/-- Composition of `f : HomObj F G A` with `g : HomObj G M A`. -/
@[simps]
def comp {M : C ⥤ D} (f : HomObj F G A) (g : HomObj G M A) : HomObj F M A where app X a := f.app X a ≫ g.app X a

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

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

Разделы

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

Аффилиация

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