English
For F ⊣ G, F′ ⊣ G, F″ ⊣ G, and x ∈ C, the app-level transitivity holds: (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x = (leftAdjointUniq adj1 adj3).hom.app x.
Русский
Для F ⊣ G, F′ ⊣ G, F″ ⊣ G и x ∈ C выполняется переходное равенство на компонентах: (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x = (leftAdjointUniq adj1 adj3).hom.app x.
LaTeX
$$$$ (leftAdjointUniq adj1 adj2).hom.app x \; \circ \; (leftAdjointUniq adj2 adj3).hom.app x = (leftAdjointUniq adj1 adj3).hom.app x, $$$$
Lean4
@[reassoc (attr := simp)]
theorem leftAdjointUniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G)
(x : C) :
(leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
(leftAdjointUniq adj1 adj3).hom.app x :=
by
rw [← leftAdjointUniq_trans adj1 adj2 adj3]
rfl
