rightAdjointUniq_hom_app_counit — Mathlib

English

For F : C ⥤ D, G, G′ : D ⥤ C, the relation between left and right adjoints gives: (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x.

Русский

Пусть F : C ⥤ D, G, G′ : D ⥤ C; тогда встречаются соответствующие коуниты: (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x.

LaTeX

$$$$ (leftAdjointUniq adj1 adj2).hom.app (G.obj x) \; \circ \; \epsilon^{(2)}_x = \epsilon^{(1)}_x, $$$$

Lean4

@[reassoc (attr := simp)]
theorem rightAdjointUniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :
    F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x := by simp [rightAdjointUniq]

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