leftKanExtensionCompIsoOfPreserves_inv_fac

English

App-level preservation follows from the universal property of the left Kan extension.

Русский

Сохранение на уровне приложений следует из универсального свойства левого кан-расширения.

LaTeX

$$$\text{PreservesLeftKanExtension_hom_fac_app}$$$

Lean4

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

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