inv_hom_id_tensor' — Mathlib

English

For a morphism f: V → W that is an isomorphism, (inv f ⊗ g) ≫ (f ⊗ h) = (id_W ⊗ g) ∘ (id_W ⊗ h).

Русский

Для тождественного изоморфизма f: V → W верно (inv f ⊗ 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) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
    (inv f ⊗ₘ g) ≫ (f ⊗ₘ h) = (𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h) := by simp

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