pseudo_surjective_of_epi — Mathlib

English

If a morphism is an epi, it is surjective on pseudoelements; conversely surjectivity implies epi.

Русский

Если морфизм является эпиморфизмом, он сюръективен на псевдоэлементах; наоборот сюръективность имплицитно эквивалентна эпи.

LaTeX

$$$\\text{epi}(f) \\iff \\mathrm{pseudo_surjective}(f)$$$

Lean4

/-- An epimorphism is surjective on pseudoelements. -/
theorem pseudo_surjective_of_epi {P Q : C} (f : P ⟶ Q) [Epi f] : Function.Surjective f := fun qbar =>
  Quotient.inductionOn qbar fun q =>
    ⟨(pullback.fst f q.hom : Over P),
      Quotient.sound <|
        ⟨pullback f q.hom, 𝟙 (pullback f q.hom), pullback.snd _ _, inferInstance, inferInstance, by
          rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]⟩⟩

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