lift_fst — Mathlib

English

Let t be a PullbackCone for f: X → Z and g: Y → Z, ht an IsLimit. For h: W → X, k: W → Y, and w: h ≫ f = k ≫ g, the universal arrow IsLimit.lift ht h k w satisfies (IsLimit.lift ht h k w) ≫ fst t = h.

Русский

Пусть t — пуллбэк-конус к f: X → Z и g: Y → Z, ht — IsLimit. При наличии h: W → X, k: W → Y и w: h ≫ f = k ≫ g, соответствующий единственный стрелок IsLimit.lift ht h k w удовлетворяет (IsLimit.lift ht h k w) ≫ fst t = h.

LaTeX

$$$\\mathrm{IsLimit.lift}\\, ht\\, h\\, k\\, w\\; \\circ\\; \\mathrm{fst}(t) = h$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_fst {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
    IsLimit.lift ht h k w ≫ fst t = h :=
  ht.fac _ _

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