lift_comp_eqToHom_iff — Mathlib

English

Let p be a functor. If φ lifts f and both are isomorphisms, then composing f with an equality-adjusted morphism preserves lifting: p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ for h: S = S'.

Русский

Пусть p — функтор. Если φ поднимает f и оба являются изоморфизмами, то композиция f с каноническим изоморфизмом, полученным из равенства, сохраняет подъем: p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ для h: S = S'.

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

@[simp]
theorem lift_comp_eqToHom_iff {R S S' : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S') :
    p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ
    where
  mp := fun hφ' => by subst h; simpa using hφ'
  mpr := fun _ => inferInstance

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