English
If φ is an isomorphism lifting f and both are isomorphisms, then composing f with an equality-induced morphism lifts as well, i.e., p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ.
Русский
Если φ является изоморфизмом, поднимающим f, и оба изоморфизмa, тогда композиция f со стрелкой, индуцированной равенством, тоже поднимается: p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ.
LaTeX
$$$\forall {R S S' : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S'),\ p.IsHomLift (f ≫ eqToHom h) φ ⟂\iff p.IsHomLift f φ$$$
Lean4
/-- Given `φ : a ≅ b` and `f : R ⟶ S`, such that `φ.hom` lifts `f`, then `φ.inv` lifts the
inverse of `f` given by `isoOfIsoLift`. -/
instance inv_lift (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] : p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv :=
by
apply of_commSq
apply CommSq.horiz_inv (f := p.mapIso φ) (by apply commSq p f φ.hom)
