coprod_inr_rightDistrib_hom — Mathlib

English

The right coprojection composed with the right-distributivity morphism equals the right-whiskered left injection, i.e., coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X.

Русский

Правая копроекция, затем ∂R X Y Z даёт копрод-инъекцию справа после перемножения справа: coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X.

LaTeX

$$$\\operatorname{coprod.inr} \\circ (\\partial_R X Y Z)^{\\mathrm{hom}} = \\operatorname{coprod.inr} \\triangleright X$$$

Lean4

@[reassoc (attr := simp)]
theorem coprod_inr_rightDistrib_hom [IsMonoidalRightDistrib C] {X Y Z : C} :
    coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X := by rw [rightDistrib_hom, coprod.inr_desc]

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