tensor_hom_inv_id' — Mathlib

English

If f: V → W is an isomorphism, then (g ⊗ f.hom) ≫ (h ⊗ inv f) = (id_V ⊗ g) ≫ (id_V ⊗ h).

Русский

Если f: V → W — изоморфизм, тогда (g ⊗ f.hom) ∘ (h ⊗ inv f) = (id_V ⊗ g) ∘ (id_V ⊗ h).

LaTeX

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

Lean4

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

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