effectiveEpi_of_map — Mathlib

English

Let F: C → D be a functor that reflects effective epis. If f: X → Y is a morphism in C and F.map f is an effective epi in D, then f is an effective epi in C.

Русский

Пусть F: C → D — функтор, отражающий эффективные эпиморфизмы. Если f: X → Y — морфизм в C и F.map f — эффективный эпиморфизм в D, тогда f — эффективный эпиморфизм в C.

LaTeX

$$$\\forall {C} [\\mathbf{Category} C] {D} [\\mathbf{Category} D] (F : C \\to D) [F.ReflectsEffectiveEpis] {X Y : C} (f : X \\to Y),\\; \\operatorname{EffectiveEpi}(F.map f) \\Rightarrow \\operatorname{EffectiveEpi}(f)$$

Lean4

theorem effectiveEpi_of_map (F : C ⥤ D) [F.ReflectsEffectiveEpis] {X Y : C} (f : X ⟶ Y) (h : EffectiveEpi (F.map f)) :
    EffectiveEpi f :=
  ReflectsEffectiveEpis.reflects f h

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