English
In a left distributive setting, the composition of (coprod.inl ▷ X) with the inverse of ∂R yields the left coprojection—the inverse distributivity isomorphism is recovered by whiskering.
Русский
В условиях левого распределения композиция (coprod.inl ▷ X) с обратным ∂R восстанавливает левую копроекцию, т.е. обратное распределение восстанавливается оснасткой.
LaTeX
$$$(\\operatorname{coprod.inl} \\otimes X) \\circ (\\partial_R X Y Z)^{-1} = \\operatorname{coprod.inl}$$$
Lean4
/-- The composite of `(coprod.inl ▷ X) : Y ⊗ X ⟶ (Y ⨿ Z) ⊗ X` and
`(∂R X Y Z).inv : (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)` is equal to the left coprojection
`coprod.inl : Y ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X)`. -/
@[reassoc (attr := simp)]
theorem whiskerRight_coprod_inl_rightDistrib_inv [IsMonoidalRightDistrib C] {X Y Z : C} :
(coprod.inl ▷ X) ≫ (∂R X Y Z).inv = coprod.inl :=
by
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
rw [assoc, Iso.inv_hom_id, comp_id, coprod_inl_rightDistrib_hom]
