Lean4
/-- (Implementation)
The evaluation of `F.lan` at `X` is the colimit over the costructured arrows over `X`.
-/
noncomputable def lanEvaluationIsoColim (F : C ⥤ D) (X : D) [∀ X : D, HasColimitsOfShape (CostructuredArrow F X) E] :
F.lan ⋙ (evaluation D E).obj X ≅ (Functor.whiskeringLeft _ _ E).obj (CostructuredArrow.proj F X) ⋙ colim :=
NatIso.ofComponents
(fun G =>
IsColimit.coconePointUniqueUpToIso (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G X)
(colimit.isColimit _))
(fun {G₁ G₂} φ => by
apply (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G₁ X).hom_ext
intro T
have h₁ := fun (G : C ⥤ E) =>
IsColimit.comp_coconePointUniqueUpToIso_hom (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G X)
(colimit.isColimit _) T
have h₂ := congr_app (F.lanUnit.naturality φ) T.left
dsimp at h₁ h₂ ⊢
simp only [Category.assoc] at h₁ ⊢
simp only [Functor.lan, Functor.lanUnit] at h₂ ⊢
rw [reassoc_of% h₁, NatTrans.naturality_assoc, ← reassoc_of% h₂, h₁, ι_colimMap, Functor.whiskerLeft_app]
rfl)
