preservesPointwiseRightKanExtensionAtOfPreservesLimit

English

If the limit of the structured arrow projection composed with F is preserved by G, then G preserves the pointwise right Kan extension of F along L at c.

Русский

Если предел проекции структурированного стрелка, сведённой к F, сохраняется G, тогда G сохраняет точечное правое Кан-расширение F вдоль L в точке c.

LaTeX

$$$\\forall c, [Limits.PreservesLimit (StructuredArrow.proj\\ c L \\circ F)\\ G] \\Rightarrow G.PreservesPointwiseRightKanExtensionAt F L c.$$$

Lean4

/-- A functor that preserves the limit of `(StructuredArrow.proj L c ⋙ F)` preserves
the pointwise right Kan extension of `F` along `L` at c. -/
instance preservesPointwiseRightKanExtensionAtOfPreservesLimit (c : C)
    [Limits.PreservesLimit (StructuredArrow.proj c L ⋙ F) G] : G.PreservesPointwiseRightKanExtensionAt F L c where
  preserves E
    p := ⟨Limits.IsLimit.ofIsoLimit (Limits.PreservesLimit.preserves p).some (E.coneAtWhiskerRightIso G _ _ c).symm⟩

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