ranCounit_app_app_ranAdjunction_unit_app_app

English

For G and X, the equality ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 1.

Русский

Для G и X выполняется: ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 1.

LaTeX

$$$((L.ranAdjunction H).unit.app G).app (L.obj X) \\;\\circ\\; (L.ranCounit.app (L \\circ G)).app X = \\mathrm{id}_{(L \\circ G).obj X}$$$

Lean4

@[reassoc (attr := simp)]
theorem ranCounit_app_app_ranAdjunction_unit_app_app (G : D ⥤ H) (X : C) :
    ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 𝟙 _ :=
  congr_app (L.ranCounit_app_whiskerLeft_ranAdjunction_unit_app G) X

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