isIso_counit_app_iff_mem_essImage

English

If there exists an iso X ≅ L.obj Y, then h.counit.app X is an isomorphism.

Русский

Если существует изоморфизм X ≅ L.obj Y, то h.counit.app X — изоморфизм.

LaTeX

$$$\forall X:\ D, \forall Y:\ C, (X \cong L.obj Y) \Rightarrow IsIso(h.counit.app X)$$$

Lean4

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

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