inl_desc — Mathlib

English

In a pushout, the inl arrow composed with the universal morphism desc is the given map h.

Русский

В точке-смещении (pushout) стрелка inl после описывающей стрелки desc равна исходной стрелке h.

LaTeX

$$$ inl \circ hP.desc h k w = h $$$

Lean4

@[reassoc (attr := simp)]
theorem inl_desc (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : f ≫ h = g ≫ k) :
    inl ≫ hP.desc h k w = h :=
  PushoutCocone.IsColimit.inl_desc hP.isColimit h k w

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