mono_comp_iff_of_isIso — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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