tensor_inv_hom_id' — Mathlib

English

For a morphism f: V → W with IsIso f, (g ⊗ inv f) ≫ (h ⊗ f) = (id_W ⊗ g) ≫ (id_W ⊗ h).

Русский

Для morphism f: V → W с существующим обратным, (g ⊗ f^{-1}) ∘ (h ⊗ f) = (id_W ⊗ g) ∘ (id_W ⊗ h).

LaTeX

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

Lean4

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

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