isIso_ranAdjunction_unit_app_iff — Mathlib

English

There is an equivalence between the unit of the ranAdjunction being an isomorphism and F being a right Kan extension of Id along L ⋙ G.

Русский

Существуют эквивалентности между тем, что единица ranAdjunction является изоморфизмом, и тем, что F является правым каноническим расширением Id вдоль L ⋙ G.

LaTeX

$$$ \\operatorname{IsIso}((L.ranAdjunction H).unit.app G) \\iff G.IsRightKanExtension(\\mathbf{1}_{L \\circ G}).$$$

Lean4

theorem isIso_ranAdjunction_unit_app_iff (G : D ⥤ H) :
    IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G)) :=
  (isRightKanExtension_iff_isIso _ (L.ranCounit.app (L ⋙ G)) _ (by simp)).symm

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