map_isHomLift — Mathlib

English

If f, φ are strongly Cartesian, then the induced morphism map p f φ hf' φ' is a lift of g along p.

Русский

Если f, φ образуют сильно-Картезианский пары, то индуцированное отображение map p f φ hf' φ' является подъемом χ вдоль p.

LaTeX

$$$\\text{IsStronglyCartesian}(p,f,\\phi) \\Rightarrow \\text{IsHomLift}(p,g,\\text{map}(p,f,\\phi,hf',\\phi')).$$$

Lean4

instance map_isHomLift : IsHomLift p g (map p f φ hf' φ') :=
  (Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.1

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