tensor_hom_inv_id — Mathlib

English

Let f be an isomorphism f: V ≅ W. For any g: X → Y and h: Y → Z, the following holds: (g ⊗ f.hom) ∘ (h ⊗ f.inv) = (g ⊗ id_V) ∘ (h ⊗ id_V).

Русский

Пусть f: V ≅ W — изоморфизм. Для любых g: X → Y и h: Y → Z выполняется (g ⊗ f.hom) ∘ (h ⊗ f.inv) = (g ⊗ id_V) ∘ (h ⊗ id_V).

LaTeX

$$$(g \\otimes f_{\\mathrm{hom}}) \\circ (h \\otimes f_{\\mathrm{inv}}) = (g \\otimes \\mathrm{Id}_V) \\circ (h \\otimes \\mathrm{Id}_V).$$$

Lean4

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

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