unit_obj_eq_map_unit — Mathlib

English

For a reflective i with left adjoint L, the unit satisfies η_iL = iL η in the sense of naturality.

Русский

Для отражателя i с левым сопряжением L равенство η_iL = iL η выполняется как естественная тождественность.

LaTeX

$$$\\eta_{iL} = iL\\,\\eta$ (на натуральной шкале)$$

Lean4

/-- For a reflective functor `i` (with left adjoint `L`), with unit `η`, we have `η_iL = iL η`.
-/
theorem unit_obj_eq_map_unit [Reflective i] (X : C) :
    (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) =
      i.map ((reflector i).map ((reflectorAdjunction i).unit.app X)) :=
  by
  rw [← cancel_mono (i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))), ← i.map_comp]
  simp

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