essSurj_of_iso — Mathlib

English

If F ≅ G and F is essentially surjective, then G is essentially surjective.

Русский

Если F и G изоморфны и F эссенциально сюръжен, то G тоже эссенциально сюръжен.

LaTeX

$$$(F \cong G) \land \operatorname{EssSurj}(F) \Rightarrow \operatorname{EssSurj}(G)$$$

Lean4

theorem essSurj_of_iso {F G : C ⥤ D} [EssSurj F] (α : F ≅ G) : EssSurj G where
  mem_essImage Y := Functor.essImage.ofNatIso α (EssSurj.mem_essImage Y)

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