preservesPointwiseLeftKanExtensionAtOfPreservesColimit

English

If G preserves the colimit of CostructuredArrow.proj L c ⋙ F, then G preserves the pointwise left Kan extension at c.

Русский

Если G сохраняет колимит CostructuredArrow.proj L c ⋙ F, тогда G сохраняет точечное левое кан-расширение в c.

LaTeX

$$$\operatorname{PreservesPointwiseLeftKanExtensionAt}(G,F,L,c)$$$

Lean4

/-- A functor that preserves the colimit of `CostructuredArrow.proj L c ⋙ F` preserves
the pointwise left Kan extension of `F` along `L` at `c`. -/
instance preservesPointwiseLeftKanExtensionAtOfPreservesColimit (c : C)
    [Limits.PreservesColimit (CostructuredArrow.proj L c ⋙ F) G] : G.PreservesPointwiseLeftKanExtensionAt F L c where
  preserves E
    p :=
    ⟨Limits.IsColimit.ofIsoColimit (Limits.PreservesColimit.preserves p).some (E.coconeAtWhiskerRightIso G _ _ c).symm⟩

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