isHomLift_iff — Mathlib

English

For a based functor F, lifting of φ by f is equivalent to lifting of F.map φ by f.

Русский

Для основанного функторa F подъем φ над f эквивалентен подъему F.map φ над f.

LaTeX

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

Lean4

theorem isHomLift_iff : IsHomLift 𝒴.p f (F.map φ) ↔ IsHomLift 𝒳.p f φ :=
  ⟨fun _ ↦ isHomLift_map F f φ, fun _ ↦ preserves_isHomLift F f φ⟩

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