lift_fst — Mathlib

English

In a pullback diagram of f,g: X → Z, with W → X and W → Y and a commuting relation h ≫ f = k ≫ g, the induced map from W to the pullback composed with the first projection equals h.

Русский

В диаграмме pullback для f,g: X → Z, при сомножении h: W → X и k: W → Y с условием h ≫ f = k ≫ g, полученное отображение из W в проекцию fst композиционно равно h.

LaTeX

$$$\mathrm{pullback.lift} h\ k\ w \;\;_{f,g} \;\; \;\; \;\;\; \; \; \; \; \; \; \; \; \; \; \; \; \; \; = h \;\;\Rightarrow\; \; \; \; \; \; \; \; \,\; \;\; \; \; \; \; \; \; \;\; \; \; \; \; \; \; \; \;\; \; \; \; $$$

Lean4

@[reassoc]
theorem lift_fst {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : h ≫ f = k ≫ g) :
    pullback.lift h k w ≫ pullback.fst f g = h :=
  limit.lift_π _ _

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