pointwiseLeftKanExtension — Mathlib

Lean4
/-- The constructed pointwise left Kan extension when `HasPointwiseLeftKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseLeftKanExtension : D ⥤ H
    where
  obj Y := colimit (CostructuredArrow.proj L Y ⋙ F)
  map {Y₁ Y₂}
    f :=
    colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
      (Cocone.mk (colimit (CostructuredArrow.proj L Y₂ ⋙ F))
        { app := fun g => colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g)
          naturality := fun g₁ g₂ φ => by
            simpa using colimit.w (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).map φ) })
  map_id
    Y :=
    colimit.hom_ext
      (fun j => by
        dsimp
        simp only [colimit.ι_desc, comp_id]
        congr
        apply CostructuredArrow.map_id)
  map_comp {Y₁ Y₂ Y₃} f
    f' :=
    colimit.hom_ext
      (fun j => by
        dsimp
        simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]
        congr 1
        apply CostructuredArrow.map_comp)
Похожие утверждения