unop_tensorμ — Mathlib

English

In the opposite category, the tensor μ morphism corresponds to the tensor μ after applying opposites componentwise.

Русский

В противоположной категории морфизм tensor μ соответствует tensor μ после применения противоположных объектов по компонентам.

LaTeX

$$$$ (tensorμ X W Y Z).unop = tensorμ X.unop Y.unop W.unop Z.unop. $$$$

Lean4

@[simp]
theorem unop_tensorμ {C : Type*} [Category C] [MonoidalCategory C] [BraidedCategory C] (X Y W Z : Cᵒᵖ) :
    (tensorμ X W Y Z).unop = tensorμ X.unop Y.unop W.unop Z.unop := by
  simp only [unop_tensorObj, tensorμ, unop_comp, unop_inv_associator, unop_whiskerLeft, unop_hom_associator,
    unop_whiskerRight, unop_hom_braiding, Category.assoc]

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