isIso_of_lift_isIso — Mathlib

English

If φ : a ⟶ b is an isomorphism and f : R ⟶ S lifts φ via p, then f is an isomorphism as well.

Русский

Если φ : a ⟶ b — изоморфизм и f : R ⟶ S поднимает φ через p, то f также изоморфизм.

LaTeX

$$$\forall {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b)\ [p.IsHomLift f φ] [IsIso φ], IsIso f$$$

Lean4

/-- If `φ : a ⟶ b` lifts `f : R ⟶ S` and `φ` is an isomorphism, then so is `f`. -/
theorem isIso_of_lift_isIso (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] [IsIso φ] : IsIso f :=
  (fac p f φ) ▸ inferInstance

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