rightAdjointUniq_hom_counit — Mathlib

English

Let F ⊣ G, F ⊣ G′, with adj1, adj2. Then the composition of the rightAdjointUniq morphisms at x corresponds to the rightAdjointUniq morphism between adj1 and adj3: (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x = (rightAdjointUniq adj1 adj3).hom.app x.

Русский

Пусть F ⊣ G, F ⊣ G′; тогда композиция морфизмов rightAdjointUniq соответствует правому уникальному морфизму между adj1 и adj3.

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_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit :=
  by
  ext
  simp

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