English
Let F ⊣ G and F′ ⊣ G be two left adjoints to the same right adjoint G. Then the counits are compatible with the unique morphism produced by leftAdjointUniq: whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit.
Русский
Пусть F ⊣ G и F′ ⊣ G — две левые сопряжённости к одному правому сопряжению. Тогда коуниты связаны с уникальным морфизмом, полученным через leftAdjointUniq: whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit.
LaTeX
$$$$ \text{whiskerLeft } G \big( (leftAdjointUniq\ adj1\ adj2).hom \big) \; \counit = \text{counit}$$$$
Lean4
@[reassoc (attr := simp)]
theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit :=
by
ext x
simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom, conjugateIsoEquiv_symm_apply_inv,
Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app, conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id,
Category.id_comp, Category.assoc]
rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
simp
