tensor_inv_hom_id — Mathlib

English

For an isomorphism f: V ≅ W and morphisms g: X → Y, h: Y → Z, we have (g ⊗ f.inv) ∘ (h ⊗ f.hom) = (g ⊗ id_W) ∘ (h ⊗ id_W).

Русский

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

LaTeX

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

Lean4

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

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