map_comp_inl_inr_codiag — Mathlib

English

The composition coprod.desc (g ≫ inl) (g' ≫ inr) equals coprod.map g g' when appropriate coproducts exist; i.e., desc ∘ (g ∘ inl) and desc ∘ (g' ∘ inr) coincide with 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

@[reassoc]
theorem map_comp_inl_inr_codiag [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y)
    (g' : X' ⟶ Y') : coprod.map (g ≫ coprod.inl) (g' ≫ coprod.inr) ≫ codiag (Y ⨿ Y') = coprod.map g g' := by simp

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