epi_of_epi — Mathlib

English

In any category, if f: X → Y and g: Y → Z with the composite f ∘ g being an epimorphism, then g is an epimorphism.

Русский

В произвольной категории, если f: X → Y и g: Y → Z such that композиция f ∘ g является эпиморфизмом, то g — эпиморфизм.

LaTeX

$$$$\\forall X,Y,Z \\; \\forall f:X\\to Y \\; \\forall g:Y\\to Z,\\; \\mathrm{Epi}(f\\circ g) \\Rightarrow \\mathrm{Epi}(g).$$$$

Lean4

theorem epi_of_epi {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi (f ≫ g)] : Epi g :=
  ⟨fun _ _ w => (cancel_epi (f ≫ g)).1 <| by simp only [Category.assoc, w]⟩

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