isIso_lanAdjunction_counit_app_iff

English

IsIso of the counit-app is equivalent to G being a LeftKanExtension of identity through L ⋙ G.

Русский

Изоморфизм counit-app эквивалентен тому, что G является левым каноническим расширением для идентичности через L ⋙ G.

LaTeX

$$$IsIso ((L.lanAdjunction H).counit.app G) \iff G.IsLeftKanExtension (id (L \circ G))$$$

Lean4

theorem isIso_lanAdjunction_counit_app_iff (G : D ⥤ H) :
    IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G)) :=
  (isLeftKanExtension_iff_isIso _ (L.lanUnit.app (L ⋙ G)) _ (by simp)).symm

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