of_iso — Mathlib

English

If P ≅ Q and P is injective, then Q is injective (and conversely).

Русский

Если P ≅ Q и P инъективен, то Q инъективен (и наоборот).

LaTeX

$$$$\text{Injective}(P) \iff \text{Injective}(Q) \text{ for } P \cong Q.$$$$

Lean4

theorem of_iso {P Q : C} (i : P ≅ Q) (hP : Injective P) : Injective Q :=
  {
    factors := fun g f mono =>
      by
      obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono
      refine ⟨h ≫ i.hom, ?_⟩
      rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id] }

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