pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac

English

If G preserves pointwise right Kan extensions and L has a pointwise right Kan extension for F, then the corresponding composition F ⋙ G has a pointwise right Kan extension along L.

Русский

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

LaTeX

$$$[PreservesPointwiseRightKanExtension G F L] \\land [L.HasPointwiseRightKanExtension F] \\Rightarrow [L.HasPointwiseRightKanExtension (F \\cdot G)].$$$

Lean4

@[reassoc (attr := simp)]
theorem pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac :
    whiskerLeft L (pointwiseRightKanExtensionCompIsoOfPreserves G F L).hom ≫
        (L.pointwiseRightKanExtensionCounit <| F ⋙ G) =
      (Functor.associator _ _ _).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G :=
  by simp [pointwiseRightKanExtensionCompIsoOfPreserves]

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