English
For α: F ⟶ L' ⋙ F', F' is left Kan extension of α iff G ⋙ F' is left Kan extension of α ≫ whiskerRight e.inv ≫ (associator _ _ _).hom.
Русский
Для α: F ⟶ L' ⋙ F', F' является левым Кан-расширением α тогда и только тогда, когда G ⋙ F' является левым Кан-расширением α ≫ whiskerRight e.inv ≫ (associator _ _ _).hom.
LaTeX
$$∗ isLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv ≫ (associator _ _ _).hom)$$
Lean4
theorem isLeftKanExtension_iff_postcomp₁ (α : F ⟶ L' ⋙ F') :
F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv _ ≫ (associator _ _ _).hom) :=
by
let eq :
(LeftExtension.mk _ α).IsUniversal ≃
(LeftExtension.mk _ (α ≫ whiskerRight e.inv _ ≫ (associator _ _ _).hom)).IsUniversal :=
(LeftExtension.isUniversalPostcomp₁Equiv G e F _).trans (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
constructor
· exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
· exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩
