lift_eqToHom_comp_iff — Mathlib

English

Let p be a functor between categories. If φ lifts f.hom, then the inverse lift satisfies p.IsHomLift (eqToHom h ≫ f) φ ↔ p.IsHomLift f φ for an equality h : R' = R.

Русский

Пусть p — функтор между категориями. Если φ поднимает f.hom, то p.IsHomLift (eqToHom h ≫ f) φ эквивалентно p.IsHomLift f φ при равенстве h: R' = R.

LaTeX

$$$\forall {R' R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R),\ p.IsHomLift (eqToHom h ≫ f) φ \iff p.IsHomLift f φ$$$

Lean4

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

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