inl_desc — Mathlib

English

In a pushout square with maps f,g and h,k satisfying f ≫ h = g ≫ k, the universal map from Y into the pushout composed with the left leg equals h.

Русский

В квадрате пушпойнта, где есть карты f,g и пары h,k с условием f ≫ h = g ≫ k, композиция Inl с Desc равна h.

LaTeX

$$$\mathrm{pushout.inl} f g \;\; ≫ \; \mathrm{pushout.desc} h k w = h.$$$

Lean4

@[reassoc]
theorem inl_desc {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
    pushout.inl _ _ ≫ pushout.desc h k w = h :=
  colimit.ι_desc _ _

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