tensorμ_natural_right — Mathlib

English

A simplified version of the left naturality of tensor product: whiskering and tensoring commute up to simp simplifications.

Русский

Упрощённая версия левой натуральности тензора: обвязывание и тензорирование приводят к одинаковому результату по упрощениям.

LaTeX

$$$$ (f_1 ⊗ f_2) ▷ (Z_1 ⊗ Z_2) = (f_1 ▷ Z_1) ⊗ (f_2 ▷ Z_2). $$$$

Lean4

@[reassoc]
theorem tensorμ_natural_right (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) :
    (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂) := by
  convert tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1 <;> simp

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