English
Let C be a monoidal category with binary coproducts. For objects X, Y, Z in C, the left distributivity morphism ∂L X Y Z expresses X ⊗ (Y ⨿ Z) as the coproduct (X ⊗ Y) ⨿ (X ⊗ Z). The compatibility with the left injection is: the left coprojection through the left distributivity is equal to the left whiskering by X of the injection.
Русский
Пусть C — моноидальная категория с парой двоичных копроизведений. Для объектов X, Y, Z в C отображение ∂L X Y Z задаёт изоморфность X ⊗ (Y ⨿ Z) ≅ (X ⊗ Y) ⨿ (X ⊗ Z). Совместимость с левой инъекцией выражается равенством: левая вложенная копроизведение через ∂L совпадает с левым точками X от инъекции coprod.
LaTeX
$$$\\operatorname{coprod.inl} \\circ (\\partial_L X Y Z)^{\\mathrm{hom}} = X \\otimes \\operatorname{coprod.inl}$$$
Lean4
@[reassoc (attr := simp)]
theorem coprod_inl_leftDistrib_hom [IsMonoidalLeftDistrib C] {X Y Z : C} :
coprod.inl ≫ (∂L X Y Z).hom = X ◁ coprod.inl := by rw [leftDistrib_hom, coprod.inl_desc]
