unit_rightAdjointUniq_hom — Mathlib

English

Let F ⊣ G and F ⊣ G′. Then the left unit of F, composed with whiskering by the rightAdjointUniq hom, equals the unit of the second adjunction: adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit.

Русский

Пусть F ⊣ G и F ⊣ G′. Тогда единица левой стороны, взятая с правой уникальностью, равна единице второй сопряжённости: adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit.

LaTeX

$$$$ adj1.unit \; \circ \; whiskerLeft F ( (rightAdjointUniq adj1 adj2).hom ) = adj2.unit, $$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_rightAdjointUniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit :=
  by
  ext x
  simp

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