rightAdjointUniq_trans_app — Mathlib

English

At object x, the componentwise composition of rightAdjointUniq homs equals the rightAdjointUniq hom between adj1 and adj3: (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x = (rightAdjointUniq adj1 adj3).hom.app x.

Русский

В точке x компоненты соответствующих правых уникальных морфизмов compose равны: ...

LaTeX

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

Lean4

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

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