hasRightKanExtension_of_preserves

English

If G preserves the pointwise right Kan extension of F along L at every c, then G preserves the general right Kan extension of F along L.

Русский

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

LaTeX

$$$\\big(\\forall c, G.PreservesPointwiseRightKanExtensionAt F L c\\big) \\Rightarrow G.PreservesRightKanExtension F L.$$$

Lean4

instance hasRightKanExtension_of_preserves [L.HasRightKanExtension F] [PreservesRightKanExtension G F L] :
    L.HasRightKanExtension (F ⋙ G) :=
  @HasRightKanExtension.mk _ _ _ _ _ _ _ _ _ _ <|
    letI : (L.rightKanExtension F).IsRightKanExtension <| L.rightKanExtensionCounit F := by infer_instance
    PreservesRightKanExtension.preserves (L.rightKanExtension F) (L.rightKanExtensionCounit F)

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