epi_of_pseudo_surjective — Mathlib

English

A morphism is epi if it is surjective on pseudoelements.

Русский

Морфизм является эпиморфизмом, если он сюръективен на псевдоэлементах.

LaTeX

$$$\\text{epi}(f) \\leftarrow\\rightarrow \\mathrm{pseudoSurjective}(f)$$$

Lean4

/-- A morphism that is surjective on pseudoelements is an epimorphism. -/
theorem epi_of_pseudo_surjective {P Q : C} (f : P ⟶ Q) : Function.Surjective f → Epi f :=
  by
  intro h
  have ⟨pbar, hpbar⟩ := h (𝟙 Q)
  have ⟨p, hp⟩ := Quotient.exists_rep pbar
  have : (⟦(p.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(𝟙 Q)⟧ :=
    by
    rw [← hp] at hpbar
    exact hpbar
  have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
  apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey
  dsimp at comm
  rw [Category.assoc, comm]
  apply Category.comp_id

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