rightAdjointUniq_trans — Mathlib

English

For F ⊣ G, F ⊣ G′, F ⊣ G″, the rightAdjointUniq morphisms compose associatively: (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom.

Русский

Пусть F ⊣ G, F ⊣ G′, F ⊣ G″. Тогда композиция соответствующих правых уникальных морфизмов удовлетворяет ассоциации: ...

LaTeX

$$$$ (rightAdjointUniq adj1 adj2).hom \; \circ \; (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom, $$$$

Lean4

@[reassoc (attr := simp)]
theorem rightAdjointUniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') :
    (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom := by
  simp [rightAdjointUniq]

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