homFrom

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom

Lean4

/-- The (unique) morphism from a pointwise left Kan extension. -/
def homFrom (G : LeftExtension L F) : E ⟶ G :=
  StructuredArrow.homMk
    { app := fun Y => (h Y).desc (LeftExtension.coconeAt G Y)
      naturality := fun Y₁ Y₂ φ =>
        (h Y₁).hom_ext
          (fun X => by
            rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]
            simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)) }
    (by
      ext X
      simpa using (h (L.obj X)).fac (LeftExtension.coconeAt G _) (CostructuredArrow.mk (𝟙 _)))

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

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

Разделы

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

Аффилиация

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