isIso_unit_app_iff_mem_essImage — Mathlib

English

If R is faithful and full, then isIso_app_unit implies membership in essImage.

Русский

Если R верен и полный, то изоморфизм приложения единицы эквивалентен принадлежности к essImage.

LaTeX

$$$\big( R\text{ Faithful} \land R\text{ Full} \big) \forall Y:\ C, IsIso(h.unit.app Y) \Rightarrow R.essImage Y$$$

Lean4

theorem isIso_unit_app_iff_mem_essImage [R.Faithful] [R.Full] {Y : C} : IsIso (h.unit.app Y) ↔ R.essImage Y :=
  by
  constructor
  · intro
    exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩
  · rintro ⟨_, ⟨i⟩⟩
    rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
    infer_instance

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