unit_naturality — Mathlib

English

Let F ⊣ G be an adjunction with unit η. For every morphism f: X → Y in C, the unit is natural in X and Y, i.e. η_X followed by G(F(f)) equals f followed by η_Y.

Русский

Пусть F ⊣ G — взаимнооднозначное отображение между категориями с единицей η. Для любых морфизмов f: X → Y в C единица ведёт естественным образом по перемещению через F и G: η_X затем G(F(f)) равняется f затем η_Y.

LaTeX

$$$\eta_X \circ G(F(f)) = f \circ \eta_Y$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_naturality {X Y : C} (f : X ⟶ Y) : adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y :=
  (adj.unit.naturality f).symm

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