English
Let F ⊣ G and F ⊣ G′. Then the landed morphism obtained from rightAdjointUniq via its hom-app at x, when mapped by the corresponding unit, equals the counit of the other adjunction: (rightAdjointUniq adj1 adj2).hom.app x ≫ adj2.counit.app x = adj1.counit.app x.
Русский
Пусть F ⊣ G и F ⊣ G′. Тогда мanипуляция через правую уникальность даёт равенство между коунитом и единичной частью: (rightAdjointUniq adj1 adj2).hom.app x ≫ adj2.counit.app x = adj1.counit.app x.
LaTeX
$$$$ (rightAdjointUniq adj1 adj2).hom.app x \; \circ \; \mathrm{counit}^{(2)}_x = \mathrm{counit}^{(1)}_x, $$$$
Lean4
@[reassoc (attr := simp)]
theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) :
adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) = adj2.unit.app x :=
by
simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom, Iso.refl_hom,
conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]
rw [← adj2.unit_naturality_assoc, ← G'.map_comp]
simp
