hasLeftKanExtension_of_preserves — Mathlib

English

If L has a pointwise left Kan extension of F and G preserves them along L, then F ⋙ G has a pointwise left Kan extension along L.

Русский

Если у L имеется точечное левое кан-расширение F, и G сохраняет их вдоль L, то F ⋙ G имеет точечное левое кан-расширение вдоль L.

LaTeX

$$$[L.HasPointwiseLeftKanExtension F]\,[PreservesPointwiseLeftKanExtension G F L] \Rightarrow L.HasPointwiseLeftKanExtension (F \circ G)$$$

Lean4

instance hasLeftKanExtension_of_preserves [L.HasLeftKanExtension F] [PreservesLeftKanExtension G F L] :
    L.HasLeftKanExtension (F ⋙ G) :=
  @HasLeftKanExtension.mk _ _ _ _ _ _ _ _ _ _ <|
    letI : (L.leftKanExtension F).IsLeftKanExtension <| L.leftKanExtensionUnit F := by infer_instance
    PreservesLeftKanExtension.preserves (L.leftKanExtension F) (L.leftKanExtensionUnit F)

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