unit_leftAdjointUniq_hom_app — Mathlib

English

Let F ⊣ G and F′ ⊣ G be two left adjoints to the same right adjoint G. Then for every object x in C, the unit components are related by the unique left-adjoint morphism: adj1.unit.app x ; G.map ( (leftAdjointUniq adj1 adj2).hom.app x ) = adj2.unit.app x.

Русский

Пусть F ⊣ G и F′ ⊣ G — две левые сопряжённости к одному правому сопряжению G. Тогда для каждого x в C компонент единицы удовлетворяет: adj1.unit.app x ; G.map( (leftAdjointUniq adj1 adj2).hom.app x ) = adj2.unit.app x.

LaTeX

$$$$ \eta_{1,x} \circ G(h_x) = \eta_{2,x}, \quad h_x : F x \to F' x, $$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
    adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by
  rw [← unit_leftAdjointUniq_hom adj1 adj2]; rfl

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