id_tensor_associator_inv_naturality

English

Naturality of the id-tensor morphism with respect to associators and tensoring.

Русский

Натуральность гомоморфизма тензора единицы по отношению к ассоциатору и тензорированию.

LaTeX

$$$$ id_{X\otimes Y} \otimes h = id_X \otimes id_Y \otimes h $$$$

Lean4

@[reassoc]
theorem id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X') :
    (f ⊗ₘ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z) := by
  rw [← id_tensorHom_id, associator_inv_naturality]

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