English
If F' and F'' are isomorphic via e, and α, α' are connected by α ≫ whiskerLeft L e.hom = α', and F' is a left Kan extension of α, then F'' is a left Kan extension of α'.
Русский
Если F' и F'' изоморфны через e, и α, α' связаны равенством α ≫ whiskerLeft L e.hom = α', а F' является левым каноническим расширением α, то F'' является левым каноническим расширением α'.
LaTeX
$$$\forall e: F' ≅ F'',\; α: F ⟶ L ∘ F',\; α' : F ⟶ L ∘ F'',\; comm: α ≫ whiskerLeft L e.hom = α',\; [F'.IsLeftKanExtension α] \\Rightarrow F''.IsLeftKanExtension α'$$$
Lean4
theorem isLeftKanExtension_of_iso {F' : D ⥤ H} {F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F')
(α' : F ⟶ L ⋙ F'') (comm : α ≫ whiskerLeft L e.hom = α') [F'.IsLeftKanExtension α] : F''.IsLeftKanExtension α' where
nonempty_isUniversal := ⟨IsInitial.ofIso (F'.isUniversalOfIsLeftKanExtension α) (StructuredArrow.isoMk e comm)⟩
