braiding_naturality — Mathlib

English

Additional properties of MonoidalLinear in ModuleCat; the tensoring with a fixed module is bilinear in morphisms.

Русский

Дополнительные свойства MonoidalLinear в ModuleCat; тензорирование фиксированного модуля билинейно по отображениям.

LaTeX

$$$\\text{MonoidalLinear}_R(\\text{ModuleCat } R)$$$

Lean4

@[simp]
theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f) :=
  by
  ext : 1
  apply TensorProduct.ext'
  intro x y
  rfl

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