functorMap

Mathlib.CategoryTheory.SmallObject.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.functorMap

Lean4

/-- The functor `SmallObject.functor f S : Arrow S ⥤ Arrow S` that is part of
the small object argument for a family of morphisms `f`, on morphisms. -/
noncomputable def functorMap : functorObj f πX ⟶ functorObj f πY :=
  pushout.map _ _ _ _ τ.left (functorMapTgt f τ) (functorMapSrc f τ) (by simp) (functorMap_comm f τ)

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

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

Разделы

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

Аффилиация

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