desc_comp_inl_comp_inr — Mathlib

English

For W ⟶ X and Y ⟶ Z, the coproduct desc of (g ≫ inl) and (g' ≫ inr) equals coprod.map g g'.

Русский

desc (g ≫ inl) (g' ≫ inr) = coprod.map g g'.

LaTeX

$$$coprod.desc (g \circ coprod.inl) (g' \circ coprod.inr) = coprod.map g g'.$$$

Lean4

@[simp]
theorem desc_comp_inl_comp_inr {W X Y Z : C} [HasBinaryCoproduct W Y] [HasBinaryCoproduct X Z] (g : W ⟶ X)
    (g' : Y ⟶ Z) : coprod.desc (g ≫ coprod.inl) (g' ≫ coprod.inr) = coprod.map g g' := by rw [← coprod.map_desc];
  simp
    -- We take the right-hand side here to be simp normal form, as this way composition lemmas for
    -- `f ≫ h` and `g ≫ k` can fire (e.g. `id_comp`), while `inl_map` and `inr_map` can still work just
    -- as well.

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