inr_desc — Mathlib

English

In a pushout square with maps f,g and h,k satisfying f ≫ h = g ≫ k, the right leg composed with the pushout description equals k.

Русский

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

LaTeX

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

Lean4

@[reassoc]
theorem inr_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.inr _ _ ≫ pushout.desc h k w = k :=
  colimit.ι_desc _ _

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