leftDistrib_hom — Mathlib

English

A more detailed formulation showing the same left distributive morphism equality in the general setting.

Русский

Более подробная формулировка того же равенства морфизмов левого распределения в общем случае.

LaTeX

$$$(\\partial_L X Y Z).\\mathrm{hom} = \\mathrm{coprod.desc} (\\_ ◁ \\mathrm{coprod.inl}) (\\_ ◁ \\mathrm{coprod.inr})$$$

Lean4

/-- The forward direction of the left distributivity isomorphism is the cogap morphism
`coprod.desc (_ ◁ coprod.inl) (_ ◁ coprod.inr) : (X ⊗ Y) ⨿ (X ⊗ Z) ⟶ X ⊗ (Y ⨿ Z)`. -/
theorem leftDistrib_hom [IsMonoidalLeftDistrib C] {X Y Z : C} :
    (∂L X Y Z).hom = coprod.desc (_ ◁ coprod.inl) (_ ◁ coprod.inr) := by rfl

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