mk' — Mathlib

English

If G preserves a pointwise left Kan extension at fixed c, then G preserves all such at c.

Русский

Если G сохраняет точечное левое кан-расширение в фиксированном объекте c, то он сохраняет все такие для этого c.

LaTeX

$$$\text{PreservesPointwiseLeftKanExtensionAt}(F,L,c)$$$

Lean4

/-- If `G` preserves any pointwise left Kan extension of `F` along `L` at `c`, then it preserves
all of them. -/
theorem mk' (c : C) {E : LeftExtension L F} (hE : E.IsPointwiseLeftKanExtensionAt c)
    (hGE : (LeftExtension.postcompose₂ L F G |>.obj E).IsPointwiseLeftKanExtensionAt c) :
    G.PreservesPointwiseLeftKanExtensionAt F L c where
  preserves E'
    hE' :=
    ⟨Limits.IsColimit.ofIsoColimit hGE <|
        (E.coconeAtWhiskerRightIso G F L c) ≪≫
          (Limits.Cocones.functoriality _ _).mapIso (hE.uniqueUpToIso hE') ≪≫ (E'.coconeAtWhiskerRightIso G F L c).symm⟩

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