lift_id_inv_isIso — Mathlib

English

If φ is an isomorphism and its lift of id_S is provided, then the inverse of φ is also liftable with id_S.

Русский

Если φ — изоморфизм и подъем для id_S задан, то обратный φ тоже поднимается над id_S.

LaTeX

$$$\forall {S : 𝒮} {a b : 𝒳} (φ : a ⟶ b) [IsIso φ], p.IsHomLift (id_S) φ.hom ⟂\Rightarrow p.IsHomLift (id_S) (inv φ)$$$

Lean4

instance lift_id_inv_isIso (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b) [IsIso φ] [p.IsHomLift (𝟙 S) φ] : p.IsHomLift (𝟙 S) (inv φ) :=
  (IsIso.inv_id (X := S)) ▸ (IsHomLift.inv p _ φ)

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