English
In an abelian category, a morphism f: X → Y is an epimorphism if and only if for every A and every y: A → Y there exist A', π: A' → A with π epi and x: A' → X such that π ∘ y = x ∘ f.
Русский
В абелевой категории морфизм f: X → Y является эпиморфизмом тогда и только тогда, когда для каждого A и каждого y: A → Y существует A', π: A' → A с эпиморфизмом π и x: A' → X such that π ∘ y = x ∘ f.
LaTeX
$$$\\forall A\\,(y:A\\to Y)\\;\\exists A',\\pi:A'\\to A\\; (\\pi\\mathrm{ epi})\\; (x:A'\\to X)\\; (\\pi\\, y = x\\, f).$$$
Lean4
theorem epi_iff_surjective_up_to_refinements (f : X ⟶ Y) :
Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f :=
by
constructor
· intro _ A a
exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩
· intro hf
obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)
rw [comp_id] at fac
exact epi_of_epi_fac fac.symm
