whiskerLeft_comp_tensorHom — Mathlib

English

For f: V → W, g: X → Y and h: Y → Z, one has (V ◁ g) ≫ (f ⊗ₘ h) = f ⊗ₘ (g ≫ h).

Русский

Для f: V → W, g: X → Y и h: Y → Z выполняется (V ◁ g) ≫ (f ⊗ₘ h) = f ⊗ₘ (g ≫ h).

LaTeX

$$$ (V \\triangleleft g) \\, \\circ \\, (f \\otimes_{\\mathrm{⊗}} h) = f \\otimes_{\\mathrm{⊗}} (g \\circ h) $$$

Lean4

@[reassoc]
theorem whiskerLeft_comp_tensorHom {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (V ◁ g) ≫ (f ⊗ₘ h) = f ⊗ₘ (g ≫ h) := by simp [tensorHom_def']

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