inv — Mathlib

English

If f and φ are isomorphisms and f.hom lifts φ.hom, then inv f lifts inv φ.

Русский

Если f и φ изоморфизмы и f.hom поднимает φ.hom, то inv f поднимает inv φ.

LaTeX

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

Lean4

/-- If `φ : a ⟶ b` lifts `f : R ⟶ S` and both are isomorphisms, then `φ⁻¹` lifts `f⁻¹`. -/
protected instance inv (f : R ⟶ S) (φ : a ⟶ b) [IsIso f] [IsIso φ] [p.IsHomLift f φ] : p.IsHomLift (inv f) (inv φ) :=
  have : p.IsHomLift (asIso f).hom (asIso φ).hom := by simp_all
  IsHomLift.inv_lift_inv p (asIso f) (asIso φ)

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