desc_comp — Mathlib

English

For a binary coproduct X ⨿ Y with structure maps g: X → V, h: Y → V and a morphism f: V → W, the universal arrow desc satisfies desc g h followed by f equals desc (g ∘ f) (h ∘ f).

Русский

Для двоичного копрода X ⨿ Y с картами g: X → V, h: Y → V и стрелкой f: V → W, универсальный переход desc удовлетворяет desc g h ∘ f = desc (g ∘ f) (h ∘ f).

LaTeX

$$$\forall V,W,X,Y\; [HasBinaryCoproduct\; X\; Y],\; (f: V\to W), (g: X\to V), (h: Y\to V),\; coprod.desc g h \circ f = coprod.desc (g \circ f) (h \circ f).$$$

Lean4

@[reassoc, simp]
theorem desc_comp {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) :
    coprod.desc g h ≫ f = coprod.desc (g ≫ f) (h ≫ f) := by ext <;> simp

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