leftAdjointUniq_hom_app_counit — Mathlib

English

Let F ⊣ G and F′ ⊣ G be two left adjoints to G. Then for any x in D, the hom component of the leftAdjointUniq map composed with the counit equals the counit of adj1: (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x.

Русский

Пусть F ⊣ G и F′ ⊣ G — две левые сопряжённости к G. Тогда для любого x в Dотношение на компоненте гомоморфизма leftAdjointUniq даёт равенство: (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x.

LaTeX

$$$$ (leftAdjointUniq adj1 adj2).hom.app (G.obj x) \; \circ \; \epsilon^{(2)}_x = \epsilon^{(1)}_x, $$$$

Lean4

@[reassoc (attr := simp)]
theorem leftAdjointUniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) :
    (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x :=
  by
  rw [← leftAdjointUniq_hom_counit adj1 adj2]
  rfl

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