tensor_id — Mathlib

English

The tensor product of identity morphisms is the identity on the tensor product: 1_x ⊗ 1_y = 1_{x⊗y}.

Русский

Тензорная композиция единичных гомоморфизмов даёт единичный гомоморфизм на тензоре: 1_x ⊗ 1_y = 1_{x⊗y}.

LaTeX

$$$\\; (\\mathbb{1}_x) \\otimes_m (\\mathbb{1}_y) = \\mathbb{1}_{x \\otimes y}.$$$

Lean4

theorem tensor_id (x y : AugmentedSimplexCategory) : (𝟙 x) ⊗ₘ (𝟙 y) = 𝟙 (x ⊗ y) :=
  by
  ext
  ·
    simpa [inl, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (𝟙 x) (WithInitial.starInitial.to y) (𝟙 x) (𝟙 y))
  ·
    simpa [inr, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (WithInitial.starInitial.to x) (𝟙 y) (𝟙 x) (𝟙 y))

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