rightDistrib_of_leftDistrib — Mathlib

English

Similarly, the right distributivity isomorphism is equal to left distributivity up to a braiding in a symmetric setting.

Русский

Аналогично, правая распределительность эквивалентна левой через braiding в симметричной обстановке.

LaTeX

$$$(coprodComparison (tensorRight X) Y Z) \\; ≪≫ \\; (β_{(Y ⨿ Z) X}).hom = (coprod.map (β_Y X).hom (β_Z X).hom) ≪≫ coprodComparison (tensorLeft X) Y Z$$$

Lean4

/-- The right distributivity isomorphism of the a left distributive symmetric monoidal category
is given by `(β_ (Y ⨿ Z) X).hom ≫ (∂L X Y Z).inv ≫ (coprod.map (β_ X Y).hom (β_ X Z).hom)`. -/
@[simp]
theorem rightDistrib_of_leftDistrib [SymmetricCategory C] [IsMonoidalDistrib C] {X Y Z : C} :
    ∂R X Y Z = (coprod.mapIso (β_ Y X) (β_ Z X)) ≪≫ (∂L X Y Z) ≪≫ (β_ X (Y ⨿ Z)) := by
  ext <;> simp [leftDistrib_hom, rightDistrib_hom]

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