map_desc — Mathlib

English

The morphism coprod.map h k and coprod.desc f g satisfy a natural compatibility: coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g).

Русский

Существует совместимость между coprod.map и coprod.desc: coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g).

LaTeX

$$$\forall {S T U V W} \,[HasBinaryCoproduct U W] [HasBinaryCoproduct T V]\; (f: U \to S) (g: W \to S) (h: T \to U) (k: V \to W),\; coprod.map h k ≫ coprod.desc f g = coprod.desc (h \circ f) (k \circ g).$$$

Lean4

@[reassoc, simp]
theorem map_desc {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U)
    (k : V ⟶ W) : coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g) := by ext <;> simp

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