isHomLift_map — Mathlib

English

If the target Y-piece lifts f with F.map φ, then φ lifts f in X; i.e., lifting is detected backwards along F.

Русский

Если цель Y-пarts поднимает f для F.map φ, тогда φ поднимает f в X; подъем обнаруживается обратно через F.

LaTeX

$$$[IsHomLift 𝒴.p\\ f (F.map\\ φ)]\\;\\Rightarrow\\; [IsHomLift 𝒳.p\\ f φ]$$

Lean4

/-- For a based functor `F : 𝒳 ⟶ 𝒴`, and an arrow `φ` in `𝒳`, then `φ` lifts an arrow `f` in `𝒮`
if `F(φ)` does. -/
theorem isHomLift_map [IsHomLift 𝒴.p f (F.map φ)] : IsHomLift 𝒳.p f φ :=
  by
  apply of_fac 𝒳.p f φ (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ)) (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))
  simp [congr_hom F.w.symm, fac 𝒴.p f (F.map φ)]

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