map_effectiveEpi — Mathlib

English

If F preserves epis, then the image of an effective epi is again effective epi.

Русский

Если F сохраняет эпиморфии, то образ эффективной эпиморфии снова эффективен.

LaTeX

$$$[F.PreservesEffectiveEpis] \Rightarrow \operatorname{EffectiveEpi}(F.map f)$$$

Lean4

instance map_effectiveEpi (F : C ⥤ D) [F.PreservesEffectiveEpis] {X Y : C} (f : X ⟶ Y) [EffectiveEpi f] :
    EffectiveEpi (F.map f) :=
  PreservesEffectiveEpis.preserves f

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