of_iso — Mathlib

English

If P ≅ Q and P is projective, then Q is projective; conversely, if Q is projective and P ≅ Q, then P is projective.

Русский

Если P ≅ Q и P проективен, то Q проективен; наоборот, если Q проективен и P ≅ Q, то P проективен.

LaTeX

$$$ {P,Q:\\, C} \\; (P \\cong Q) \\Rightarrow (\\text{Projective } P \\iff \\text{Projective } Q) $$$

Lean4

theorem of_iso {P Q : C} (i : P ≅ Q) (_ : Projective P) : Projective Q where
  factors f e
    _ :=
    let ⟨f', hf'⟩ := Projective.factors (i.hom ≫ f) e
    ⟨i.inv ≫ f', by simp [hf']⟩

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