functorMap_π

Mathlib.CategoryTheory.SmallObject.Construction

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

Lean4

@[reassoc (attr := simp)]
theorem functorMap_π : functorMap f τ ≫ πFunctorObj f πY = πFunctorObj f πX ≫ τ.right :=
  by
  ext ⟨i, t, b, w⟩
  · simp [functorMap]
  · simp [functorMap, ι_functorMapTgt_assoc f τ i t b w _ rfl]

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

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

Разделы

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

Аффилиация

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