tensorHom_comp_tensorHom — Mathlib

English

Tensoring preserves composition: the tensor of two composed arrows equals the composition of their tensor images.

Русский

Тензоризация сохраняет композицию: тензор композиции равен композиции тензоров.

LaTeX

$$$\\Big( f_1 \\otimes_m f_2 \\Big) \\circ \\Big( g_1 \\otimes_m g_2 \\Big) = (f_1 \\circ g_1) \\otimes_m (f_2 \\circ g_2).$$$

Lean4

theorem tensorHom_comp_tensorHom {x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂)
    (g₁ : y₁ ⟶ z₁) (g₂ : y₂ ⟶ z₂) : (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) := by cat_disch

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