instIsIsoAppCounitObjOfFaithfulOfFull

English

If L is faithful and full, then for every Y in C, h.counit.app (L.obj Y) is an isomorphism.

Русский

Если L верный и полный, то для каждого Y ∈ C композиция h.counit на L.obj Y является изоморфизмом.

LaTeX

$$$\big( L\text{ Faithful} \land L\text{ Full} \big) \forall Y:\ C,\ IsIso\big(h.counit.app\big(L.obj Y\big)\big)$$$

Lean4

instance [L.Faithful] [L.Full] {Y : C} : IsIso (h.counit.app (L.obj Y)) :=
  isIso_of_hom_comp_eq_id _ (h.left_triangle_components Y)

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