preserves_isHomLift — Mathlib

English

If φ lifts f in X, then F.map φ lifts f in Y; i.e., lifting is preserved by the based functor.

Русский

Если φ поднимает f в X, то F.map φ поднимает f в Y; поднятие сохраняется базовым функтором.

LaTeX

$$$\\text{If } IsHomLift\\ 𝒳.p\\ f\\ φ\\;\\text{ then } IsHomLift\\ 𝒴.p\\ f\\ (F.map\\ φ)$$$

Lean4

/-- For a based functor `F : 𝒳 ⟶ 𝒴`, then whenever an arrow `φ` in `𝒳` lifts some `f` in `𝒮`,
then `F(φ)` also lifts `f`. -/
instance preserves_isHomLift [IsHomLift 𝒳.p f φ] : IsHomLift 𝒴.p f (F.map φ) :=
  by
  apply of_fac 𝒴.p f (F.map φ) (Eq.trans (F.w_obj a) (domain_eq 𝒳.p f φ)) (Eq.trans (F.w_obj b) (codomain_eq 𝒳.p f φ))
  rw [← Functor.comp_map, congr_hom F.w]
  simpa using (fac 𝒳.p f φ)

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