English
The composition of epimorphisms is an epimorphism: if f and g are epis, then f ≫ g is epi.
Русский
Композиция эпиморфизмов снова является эпиморфизмом: если f и g — эпиморфизмы, то f ≫ g — эпиморфизм.
LaTeX
$$$ \\forall {C} [\\mathrm{Category}\ C], {X Y Z} (f:X\\to Y) [\\mathrm{Epi} f] (g:Y\\to Z) [\\mathrm{Epi} g], \\mathrm{Epi}(\\mathrm{comp}(f,g)) $$$
Lean4
/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp'`. -/
instance epi_comp {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (f ≫ g) :=
⟨fun _ _ w => (cancel_epi g).1 <| (cancel_epi_assoc_iff f).1 w⟩
