English
Let p be a functor between categories. For any morphism f in the target category and any morphism φ in the source lifting f, if b equals b' then composing φ with the canonical isomorphism coming from b = b' does not change whether φ lifts f via p; i.e., p.IsHomLift f (φ ≫ eqToHom h) is equivalent to p.IsHomLift f φ.
Русский
Пусть p — функтор между категориями. Для любого морфизма f в целевой категории и для морфизма φ в исходной, который поднимает f через p, если b = b' то композиция φ с каноническим изоморфизмом, порожденным равенством h: b = b', не меняет свойство подъёма через p; тождество p.IsHomLift f (φ ≫ eqToHom h) эквивалентно p.IsHomLift f φ.
LaTeX
$$$\forall {R S : 𝒮} {a b b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b'),\ p.IsHomLift f (φ \circ \mathrm{eqToHom}(h)) \iff p.IsHomLift f φ$$$
Lean4
@[simp]
theorem eqToHom_comp_lift_iff {R S : 𝒮} {a b b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b') :
p.IsHomLift f (φ ≫ eqToHom h) ↔ p.IsHomLift f φ
where
mp hφ' := by subst h; simpa using hφ'
mpr _ := inferInstance
