pointwiseLeftKanExtensionIsPointwiseLeftKanExtension

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

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

Lean4

/-- The functor `pointwiseLeftKanExtension L F` is a pointwise left Kan
extension of `F` along `L`. -/
noncomputable def pointwiseLeftKanExtensionIsPointwiseLeftKanExtension :
    (LeftExtension.mk _ (pointwiseLeftKanExtensionUnit L F)).IsPointwiseLeftKanExtension := fun X =>
  IsColimit.ofIsoColimit (colimit.isColimit _)
    (Cocones.ext (Iso.refl _)
      (fun j => by
        dsimp
        simp only [comp_id, colimit.ι_desc, CostructuredArrow.map_mk]
        congr 1
        rw [id_comp, ← CostructuredArrow.eq_mk]))

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

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

Разделы

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

Аффилиация

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