essSurj_functor — Mathlib

English

The functor of an equivalence is essentially surjective: every object in the target category is isomorphic to the image of some object.

Русский

Функтор эквивалентности существенно сюръджентен: любой объект целевой категории изоморфен образу некоторого объекта.

LaTeX

$$$\text{EssSurj}(e.functor)$$$

Lean4

/-- The functor of an equivalence of categories is essentially surjective. -/
@[stacks 02C3]
instance essSurj_functor (e : C ≌ E) : e.functor.EssSurj :=
  ⟨fun Y => ⟨e.inverse.obj Y, ⟨e.counitIso.app Y⟩⟩⟩

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