instEssSurjCompPreRight — Mathlib

English

If F is essentially surjective, then preRight L F R is essentially surjective.

Русский

Если F является эссенциально сюръективной, то preRight L F R эссенциально сюръективна.

LaTeX

$$$F\text{ EssSurj} \Rightarrow (\text{preRight } L F R)\text{ EssSurj}$$$

Lean4

instance (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.EssSurj] : (preRight L F R).EssSurj :=
  Functor.essSurj_of_iso (preRightIso L F R).symm

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