id_tensorHom — Mathlib

English

In the localized monoidal category, tensoring with the identity morphism on the second factor acts as the left whisker of the morphism: for any morphism f: X1 → X2, and any Y, 1_X ⊗ f equals the left whiskering of f by X.

Русский

В локализованной моноидальной категории тензор с единичной морфизмом по второй компоненте действует как левое придвижение: для любого f: X1 → X2 и любого Y, 1_X ⊗ f совпадает с левым придвижением f на X.

LaTeX

$$$\\mathbf{1}_X \\otimes_\\otimes f = X \\triangleleft f$$$

Lean4

theorem id_tensorHom (X : LocalizedMonoidal L W ε) {Y₁ Y₂ : LocalizedMonoidal L W ε} (f : Y₁ ⟶ Y₂) : 𝟙 X ⊗ₘ f = X ◁ f :=
  by simp [monoidalCategoryStruct]

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