English
Let F ⊣ G, F′ ⊣ G, F″ ⊣ G be three left adjoints to the same G. Then the hom components of leftAdjointUniq satisfy the transitivity: (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom = (leftAdjointUniq adj1 adj3).hom.
Русский
Пусть три левые сопряжённости F ⊣ G, F′ ⊣ G, F″ ⊣ G. Тогда композиции соответствующих гомоморфизмов leftAdjointUniq удовлетворяют транзитивности: (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom = (leftAdjointUnqi adj1 adj3).hom.
LaTeX
$$$$ (leftAdjointUniq adj1 adj2).hom \; \circ \; (leftAdjointUniq adj2 adj3).hom = (leftAdjointUniq adj1 adj3).hom, $$$$
Lean4
@[reassoc (attr := simp)]
theorem leftAdjointUniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) :
(leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom = (leftAdjointUniq adj1 adj3).hom := by
simp [leftAdjointUniq]
