tensor_id_comp_id_tensor

Mathlib.CategoryTheory.Monoidal.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor

English

A standard rearrangement: f ≫ g ⊗ Id_Z = (f ⊗ Id_Z) ≫ (g ⊗ Id_Z).

Русский

Стандартная перестановка: f ∘ g ⊗ Id_Z = (f ⊗ Id_Z) ∘ (g ⊗ Id_Z).

LaTeX

$$$ f \\circ g \\otimes \\mathrm{Id}_Z = (f \\otimes \\mathrm{Id}_Z) \\circ (g \\otimes \\mathrm{Id}_Z).$$$

Lean4

@[reassoc]
theorem tensor_id_comp_id_tensor (f : W ⟶ X) (g : Y ⟶ Z) : (g ⊗ₘ 𝟙 W) ≫ (𝟙 Z ⊗ₘ f) = g ⊗ₘ f := by simp [tensorHom_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru