lift_extend — Mathlib

English

Let F be a diagram with a limit, c a cone over F, X an object of C, and f: X ⟶ c.pt. Then the limit lift of the extended cone c.extend f equals the composition of f with the lift of c: limit.lift F (c.extend f) = f ≫ limit.lift F c.

Русский

Пусть F имеет предел, c — конус над F, X — объект в C, и f: X ⟶ c.pt. Тогда лимит-лифтинг расширенного конуса равен композиции f с lifting конуса: limit.lift F (c.extend f) = f ≫ limit.lift F c.

LaTeX

$$$\\operatorname{limit.lift} F (c.\\mathrm{extend} f) = f \\gg \\operatorname{limit.lift} F c$$$

Lean4

theorem lift_extend {F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) :
    limit.lift F (c.extend f) = f ≫ limit.lift F c := by cat_disch

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