instIsHomLiftIdMapFiberInclusion — Mathlib

English

For a cartesian lift a f in a pseudofunctor CoGrothendieck setting, the forgetful map preserves the hom-lift structure; i.e., isHomLift cartesianLift ensures a lift to the arrow f.

Русский

Для каретизируемого подъема cartesianLift сохраняется структура подъема гом, гарантирующая подъем стрелы f.

LaTeX

$$$IsHomLift\ forget\ F\ f\ (cartesianLift\ a\ f)$$$

Lean4

instance {a b : Fiber p S} (φ : a ⟶ b) : IsHomLift p (𝟙 S) (fiberInclusion.map φ) :=
  φ.2

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