preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise

English

If there exists HasPointwiseRightKanExtension L F and G preserves pointwise right Kan extensions along F L, then G preserves right Kan extensions along L for F.

Русский

Если существует HasPointwiseRightKanExtension L F и G сохраняет точечные правые Кан-расширения вдоль F L, то G сохраняет правые Кан-расширения вдоль L для F.

LaTeX

$$$[HasPointwiseRightKanExtension L F] \\land [G.PreservesPointwiseRightKanExtension F L] \\Rightarrow G.PreservesRightKanExtension F L.$$$

Lean4

/-- If there is a pointwise right Kan extension of `F` along `L`, and if `G` preserves them,
then `G` preserves right Kan extensions of `F` along `L`. -/
instance preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise [HasPointwiseRightKanExtension L F]
    [G.PreservesPointwiseRightKanExtension F L] : G.PreservesRightKanExtension F L where
  preserves F' α
    _ :=
    (RightExtension.isPointwiseRightKanExtensionEquivOfIso (RightExtension.postcompose₂ObjMkIso G α) <|
        (isPointwiseRightKanExtensionOfIsRightKanExtension F' α).postcompose G).isRightKanExtension

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