tensorμ_natural_left — Mathlib

English

Naturalness of the left tensor with respect to morphisms f1 and f2: whiskering before tensoring commutes with tensoring of morphisms.

Русский

Природность левого тензора по отношению к морфизмам f1 и f2: предобшение перед тензорированием коммутирует с тензоризацией морфизмов.

LaTeX

$$$$ (f_1 ⟶ Y_1) \; (f_2 ⟶ Y_2) \,:\; (f_1 ⊗ f_2) \;⊢ (f_1 ⊗ f_2) ⊗ (Z_1 ⊗ Z_2) = (f_1 ⊗ g_1) ⊗ (f_2 ⊗ g_2). $$$$

Lean4

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

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