whiskerLeft_coprod_inr_leftDistrib_inv

English

Dual to the previous, in a left-distributive setting, the composition with the inverse of ∂L X Y Z on the left via coprod.inr yields the right coprojection coprod.inr.

Русский

Двойственность к предыдущему: через coprod.inr и обратную ∂L X Y Z слева получаем праовую копроекция coprod.inr.

LaTeX

$$$(X \\otimes \\operatorname{coprod.inr}) \\circ (\\partial_L X Y Z)^{-1} = \\operatorname{coprod.inr}$$$

Lean4

/-- The composite of `(X ◁ coprod.inr) : X ⊗ Z ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv :  X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the right coprojection `coprod.inr : X ⊗ Z ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`. -/
@[reassoc (attr := simp)]
theorem whiskerLeft_coprod_inr_leftDistrib_inv [IsMonoidalLeftDistrib C] {X Y Z : C} :
    (X ◁ coprod.inr) ≫ (∂L X Y Z).inv = coprod.inr :=
  by
  apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp
  rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_leftDistrib_hom]

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