lift_id_inv — Mathlib

English

If φ is an isomorphism and f is an arrow with a lift, then the inverse of isoOfIsoLift lifts the inverse morphism.

Русский

Если φ — изоморфизм и f — стрелка с подъёмом, тогда inv(isoOfIsoLift) поднимает обратный морфизм.

LaTeX

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

Lean4

/-- If `φ : a ≅ b` is an isomorphism lifting `𝟙 S` for some `S : 𝒮`, then `φ⁻¹` also
lifts `𝟙 S`. -/
instance lift_id_inv (S : 𝒮) {a b : 𝒳} (φ : a ≅ b) [p.IsHomLift (𝟙 S) φ.hom] : p.IsHomLift (𝟙 S) φ.inv :=
  have : p.IsHomLift (asIso (𝟙 S)).hom φ.hom := by simp_all
  (IsIso.inv_id (X := S)) ▸ (IsHomLift.inv_lift_inv p (asIso (𝟙 S)) φ)

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