tensorHom_comp_tensorHom — Mathlib

English

Tensoring composable morphisms distributes over composition: (f1 ⊗ f2) ≫ (g1 ⊗ g2) = (f1 ≫ g1) ⊗ (f2 ≫ g2).

Русский

Тензоризация согласна с композициями: (f1 ⊗ f2) ≫ (g1 ⊗ g2) = (f1 ≫ g1) ⊗ (f2 ≫ g2).

LaTeX

$$$ (f_1 \otimes f_2) \;\gg\; (g_1 \otimes g_2) = (f_1 \gg g_1) \otimes (f_2 \gg g_2)$$$

Lean4

theorem tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
    (g₂ : Y₂ ⟶ Z₂) : (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) := by ext <;> simp;
  ext <;> simp <;> (rw [← Category.assoc]; congr 1; simp)

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