coprod_inl_rightDistrib_hom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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