English
For isomorphic left Kan extensions F' ≅ F'' with corresponding α, α' you have F'.IsLeftKanExtension α implies F''.IsLeftKanExtension α', and conversely when using the inverse isomorphism.
Русский
Для изоморфных левых Кан_Extension F' ≅ F'' с соответствующими α, α' верно: F'.IsLeftKanExtension α влечёт F''IsLeftKanExtension α' и наоборот через обратное изоморфирование.
LaTeX
$$$(F' \cong F'') \land (comm: α ≫ whiskerLeft L e.hom = α') \;\Rightarrow\; (F'.IsLeftKanExtension α) \Rightarrow (F''.IsLeftKanExtension α')$ и обратно через симметрию.$$
Lean4
theorem isLeftKanExtension_iff_of_iso {F' 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 α' :=
by
constructor
· intro
exact isLeftKanExtension_of_iso e α α' comm
· intro
refine isLeftKanExtension_of_iso e.symm α' α ?_
rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
