epi_comp_iff_of_isIso — Mathlib

English

If g is an isomorphism, f ≫ g is epi iff f is epi.

Русский

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

LaTeX

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

Lean4

/-- When `g` is an isomorphism, `f ≫ g` is epic iff `f` is. -/
@[simp]
theorem epi_comp_iff_of_isIso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : Epi (f ≫ g) ↔ Epi f :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  simpa using (inferInstance : Epi ((f ≫ g) ≫ inv g))

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