map

Mathlib.CategoryTheory.Limits.Shapes.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.end_.map

Lean4

/-- A natural transformation of functors F ⟶ F' induces a map end_ F ⟶ end_ F'. -/
noncomputable def map : end_ F ⟶ end_ F' :=
  end_.lift (fun x ↦ end_.π _ _ ≫ (f.app (op x)).app x)
    (fun j j' φ ↦ by
      have e := (f.app (op j)).naturality φ
      simp only [Category.assoc]
      rw [← e, reassoc_of% end_.condition F φ]
      simp)

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

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

Разделы

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

Аффилиация

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