epi_comp_iff_of_epi — Mathlib

English

When f is epi, f ≫ g is epi iff g is epi.

Русский

Когда f — эпиморфизм, f ≫ g — эпиморфизм тогда и только тогда, когда g — эпиморфизм.

LaTeX

$$$ {X Y Z : C} (f : X \to Y) [\mathrm{Epi}(f)] (g : Y \to Z) : \mathrm{Epi}(f \gg g) \;\Leftrightarrow\; \mathrm{Epi}(g).$$$

Lean4

/-- When `f` is an epimorphism, `f ≫ g` is epic iff `g` is. -/
@[simp]
theorem epi_comp_iff_of_epi {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) : Epi (f ≫ g) ↔ Epi g :=
  ⟨fun _ ↦ epi_of_epi f _, fun _ ↦ inferInstance⟩

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