tensor_whiskerLeft — Mathlib

English

Let X and Y be objects and f: Z → Z' a morphism. The left whiskering by X ⊗ Y interacts with f via the associator: (X ⊗ Y) ◁ f = (α_{X,Y,Z}).hom ≫ (X ◁ Y ◁ f) ≫ (α_{X,Y,Z'}).inv.

Русский

Пусть X, Y — объекты, f: Z → Z'. Левая обертка по X ⊗ Y взаимодействует с f через ассоциатор: (X ⊗ Y) ◁ f = (α_{X,Y,Z}).hom ≫ (X ◁ Y ◁ f) ≫ (α_{X,Y,Z'}).inv.

LaTeX

$$$ (X \\otimes Y) \\triangleleft f = (\\alpha_{X,Y,Z}).hom \\circ (X \\triangleleft Y \\triangleleft f) \\circ (\\alpha_{X,Y,Z'}).inv $$$

Lean4

@[reassoc, simp]
theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
    (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv :=
  by
  simp only [← id_tensorHom]
  rw [← assoc, ← associator_naturality]
  simp

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