inv_lift_inv — Mathlib

English

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

Русский

Если f и φ являются изоморфизмами и f.hom поднимает φ.hom через p, тогда f.inv поднимает φ.inv через p.

LaTeX

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

Lean4

/-- Given `φ : a ≅ b` and `f : R ≅ S`, such that `φ.hom` lifts `f.hom`, then `φ.inv` lifts
`f.inv`. -/
instance inv_lift_inv (f : R ≅ S) (φ : a ≅ b) [p.IsHomLift f.hom φ.hom] : p.IsHomLift f.inv φ.inv :=
  by
  apply of_commSq
  apply CommSq.horiz_inv (f := p.mapIso φ) (commSq p f.hom φ.hom)

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