English
Analogous to the previous, the composition of (coprod.inr ▷ X) with the inverse of ∂L yields the right coprojection; the inverse left distributivity is recovered by whiskering.
Русский
Аналогично предыдущему: композиция (coprod.inr ▷ X) с обратной ∂L восстанавливает правую копроекцию; обратное лево-распределение восстанавливается оснасткой.
LaTeX
$$$(\\operatorname{coprod.inr} \\otimes X) \\circ (\\partial_L X Y Z)^{-1} = \\operatorname{coprod.inr}$$$
Lean4
/-- The composite of `(coprod.inr ▷ X) : Z ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv : (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the right coprojection
`coprod.inr : Z ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`. -/
@[reassoc (attr := simp)]
theorem whiskerRight_coprod_inr_rightDistrib_inv [IsMonoidalRightDistrib C] {X Y Z : C} :
(coprod.inr ▷ X) ≫ (∂R X Y Z).inv = coprod.inr :=
by
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_rightDistrib_hom]
