effectiveEpiOfKernelPair — Mathlib

English

If f: X → B has a pullback and the canonical coequalizer of its kernel pair exists, then f is an effective epi.

Русский

Если у отображения f: X → B существует соответствующий канонический коэкьюлятор для его ядра пары, и есть соответствующий ограниченный предел (допуск), то f является эффективным эпиморфизмом.

LaTeX

$$$\\forall {C} [\\mathbf{Category} C] {B X : C} (f : X \\to B) [HasPullback f f] (hc : IsColimit (Cofork.ofπ f pullback.condition)) , \\operatorname{EffectiveEpi} f$$

Lean4

/-- A morphism which is a coequalizer for its kernel pair is an effective epi. -/
theorem effectiveEpiOfKernelPair {B X : C} (f : X ⟶ B) [HasPullback f f]
    (hc : IsColimit (Cofork.ofπ f pullback.condition)) : EffectiveEpi f :=
  let _ := regularEpiOfKernelPair f hc
  inferInstance

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