lift_pre — Mathlib

English

If F is a diagram and E: K ⥤ J with HasLimit F and HasLimit (E ⋙ F), then for any cone c over F and morphism from its vertex, the lift pre satisfies: limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E).

Русский

Если F — диаграмма, E: K ⥤ J и существуют пределы F и (E ⋙ F), то для конуса c и морфизма f: c.pt ⟶ ?, имеет место: limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E).

LaTeX

$$$\\operatorname{limit.lift} F c \\gg \\operatorname{limit.pre} F E = \\operatorname{limit.lift} (E \\;\\cdot\\; F) (c.\\mathrm{whisker} E)$$$

Lean4

@[simp]
theorem lift_pre (c : Cone F) : limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) := by ext; simp

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