inv_hom_id_tensor — Mathlib

English

In a monoidal category, tensoring with an isomorphism f: V ≅ W preserves composition: for any g: X → Y and h: Y → Z, (f^{-1} ⊗ g) ∘ (f ⊗ h) = (id_W ⊗ g) ∘ (id_W ⊗ h).

Русский

В моноидальной категории тензорирование по изоморфизму f: V ≅ W сохраняет композицию: для любых g: X → Y и h: Y → Z выполняется (f^{-1} ⊗ g) ∘ (f ⊗ h) = (id_W ⊗ g) ∘ (id_W ⊗ h).

LaTeX

$$$ (f^{-1} \\otimes g) \\circ (f \\otimes h) = (\\mathrm{Id}_W \\otimes g) \\circ (\\mathrm{Id}_W \\otimes h). $$$

Lean4

@[reassoc]
theorem inv_hom_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (f.inv ⊗ₘ g) ≫ (f.hom ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h) := by simp

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