homEquiv_symm_rightAdjointUniq_hom_app

English

Let F ⊣ G and let G′ be another right adjoint with adj1 : F ⊣ G and adj2 : F ⊣ G′. Then the inverse of the homEquiv, applied to the rightAdjointUniq hom, recovers the counit: (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x.

Русский

Пусть F ⊣ G и G′ другая правая адъюнкция. Обратное отображение гомоморфий возвращает коунит: (adj2.homEquiv ...).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x.

LaTeX

$$$$ (adj2.homEquiv_{F,G}^{-1})\big((rightAdjointUniq adj1 adj2).hom.app x\big) = adj1.counit.app x, $$$$

Lean4

theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :
    (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x := by simp [rightAdjointUniq]

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