homEquiv_leftAdjointUniq_hom_app — Mathlib

English

For two left adjoints F ⊣ G and F' ⊣ G with G the same right adjoint, the hom-equivalence sends the unique morphism given by leftAdjointUniq adj1 adj2 to the unit of adj2.

Русский

Для двух левых смежных F ⊣ G и F' ⊣ G, гом-эквивариантность отправляет уникальный морфизм, заданный leftAdjointUniq adj1 adj2, в единицу adj2.

LaTeX

$$$\forall {C D},\; \text{homEquiv}_{x, (F'.obj x)}( (\text{leftAdjointUniq } adj1 adj2).\mathrm{hom}.\mathrm{app} x ) = adj2.unit.\mathrm{app} x$$$

Lean4

theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
    adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by simp [leftAdjointUniq]

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