preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise

English

If there is a HasPointwiseLeftKanExtension and G preserves pointwise, then G preserves left Kan extensions.

Русский

Если имеется точечное левое кан-расширение и G сохраняет точечные, тогда G сохраняет левое кан-расширение.

LaTeX

$$$\operatorname{PreservesLeftKanExtension}(F,L)\text{ by }G$$$

Lean4

/-- If there is a pointwise left Kan extension of `F` along `L`, and if `G` preserves them,
then `G` preserves left Kan extensions of `F` along `L`. -/
instance preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise [HasPointwiseLeftKanExtension L F]
    [G.PreservesPointwiseLeftKanExtension F L] : G.PreservesLeftKanExtension F L where
  preserves F' α
    _ :=
    (LeftExtension.isPointwiseLeftKanExtensionEquivOfIso (LeftExtension.postcompose₂ObjMkIso G α) <|
        (isPointwiseLeftKanExtensionOfIsLeftKanExtension F' α).postcompose G).isLeftKanExtension

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