map_adj₂_counit_app_leftToRight_app

English

At each X, t.adj₁.counit.app(H.obj X) followed by t.rightToLeft.app X equals F.map(t.adj₂.counit.app X).

Русский

На каждом X композиция t.adj₁.counit.app(H.obj X) с t.rightToLeft.app X равна F.map(t.adj₂.counit.app X).

LaTeX

$$$t.adj_1.counit.app (H.obj X) \;\circ\; t.rightToLeft.app X = F.map (t.adj_2.counit.app X)$$$

Lean4

theorem map_adj₂_counit_app_leftToRight_app (X : C) :
    F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X = t.adj₁.counit.app (H.obj X) := by simp

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