English
In a left-distributive monoidal category, the composition of the left whiskering (X used to act on coprod.inl) with the inverse of the left distributivity ∂L X Y Z equals the left coprojection coprod.inl.
Русский
В левораспределяющей моноидальной категории композиция левого подбора (X действует на coprod.inl) с обратной стороной левого распределения ∂L X Y Z равна левой копроекции coprod.inl.
LaTeX
$$$(X \\otimes \\operatorname{coprod.inl}) \\circ (\\partial_L X Y Z)^{-1} = \\operatorname{coprod.inl}$$$
Lean4
/-- The composite of `(X ◁ coprod.inl) : X ⊗ Y ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv : X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the left coprojection `coprod.inl : X ⊗ Y ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`. -/
@[reassoc (attr := simp)]
theorem whiskerLeft_coprod_inl_leftDistrib_inv [IsMonoidalLeftDistrib C] {X Y Z : C} :
(X ◁ coprod.inl) ≫ (∂L X Y Z).inv = coprod.inl :=
by
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp
rw [assoc, Iso.inv_hom_id, comp_id, coprod_inl_leftDistrib_hom]
