unit_leftAdjointUniq_hom — Mathlib

English

The unit for the left adjoint, when composed with the whiskerRight of the uniq-hom of adj1 and adj2, equals adj2.unit.

Русский

Единица левого смежного композитного с whiskerRight от uniq-hom adj1 adj2 равна adj2.unit.

LaTeX

$$$\text{adj1.unit} \;\gg\; \mathrm{whiskerRight}( (\mathrm{leftAdjointUniq} adj1 adj2).hom, G) = adj2.unit$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_leftAdjointUniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit :=
  by
  ext x
  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
  simp

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