hom_inv_id_tensor — Mathlib

English

Compatibility of tensoring with a pair of isomorphisms against identity morphisms on the base objects.

Русский

Совместимость тензорирования с парой изоморфизмов по отношению к гомоморфизмам-идентичностям на базовых объектах.

LaTeX

$$$$ (f.hom \otimes g) \circ (f.inv \otimes h) = (id_V \otimes g) \circ (id_V \otimes h) $$$$

Lean4

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

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