surjective_up_to_refinements_of_epi

English

If f is epi, then for any A and y: A → Y there exist a refinement as above (A', π, x) with π epi such that π ∘ y = x ∘ f.

Русский

Если f — эпиморфизм, то для любого A и любого y: A → Y существует уточнение (A', π, x) с эпиморфизмом π такое, что π ∘ y = x ∘ f.

LaTeX

$$$\\forall A\\,(y:A\\to Y),\\; \\exists A',\\pi:A'\\to A\\; (\\pi\\text{ epi})\\; (x:A'\\to X),\\; \\pi\\, y = x\\, f$$$

Lean4

theorem surjective_up_to_refinements_of_epi (f : X ⟶ Y) [Epi f] {A : C} (y : A ⟶ Y) :
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f :=
  (epi_iff_surjective_up_to_refinements f).1 inferInstance y

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