English
Let α1: F1 ⟶ L ⋙ F1' and α2: F2 ⟶ L ⋙ F2' with an iso e: F1 ≅ F2 and e': F1' ≅ F2' and a compatibility h. Then F1'.IsLeftKanExtension α1 iff F2'.IsLeftKanExtension α2.
Русский
Пусть α1: F1 ⟶ L ⋙ F1' и α2: F2 ⟶ L ⋙ F2' с изоморфизмом e: F1 ≅ F2 и e': F1' ≅ F2' и совместимостью h. Тогда F1'.IsLeftKanExtension α1 эквивално F2'.IsLeftKanExtension α2.
LaTeX
$$$F_1'.IsLeftKanExtension\\ α_1 \\iff F_2'.IsLeftKanExtension\\ α_2$$$
Lean4
theorem isLeftKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : F₁ ⟶ L ⋙ F₁') (α₂ : F₂ ⟶ L ⋙ F₂') (e : F₁ ≅ F₂)
(e' : F₁' ≅ F₂') (h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂) :
F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂ :=
by
let eq := LeftExtension.isUniversalEquivOfIso₂ (LeftExtension.mk _ α₁) (LeftExtension.mk _ α₂) e e' h
constructor
· exact fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩
· exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩
