isIso_hom — Mathlib

English

If L is full and faithful, then the hom component of the pointwise right extension is an isomorphism.

Русский

Если L полно и полнофидно, то компонент гомоморфизма в точечном правом кан-расширении является изоморфизмом.

LaTeX

$$$\operatorname{IsIso}(E.hom)$$$

Lean4

theorem isIso_hom [L.Full] [L.Faithful] : IsIso (E.hom) :=
  have := fun X => (h (L.obj X)).isIso_hom_app
  NatIso.isIso_of_isIso_app ..

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