hom_inv_id_tensor' — Mathlib

English

Let f: V → W be invertible (IsIso f). For g: X → Y and h: Y → Z, we have (f ⊗ g) ≫ (inv f ⊗ h) = (id_V ⊗ g) ≫ (id_V ⊗ h).

Русский

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

LaTeX

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

Lean4

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

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