tensor_δ — Mathlib

English

The associator in the monoidal structure for tensoring two tensor products satisfies a higher coherence condition expressed by a specific equality between two ways of inserting associators and μ maps.

Русский

Ассоциатор моноидальной структуры удовлетворяет более высокому когерентному свойству, представленному равенством между двумя способами вставки ассоциаторов и μ.

LaTeX

$$$$ (tensorμ (X_1⊗X_2) X_3 (Y_1⊗Y_2) Y_3) ≫ (tensorμ (X_1⊗Y_1) (X_2⊗Y_2) Z_1 Z_2) ≫ ((α_{X_1 Y_1 Z_1}.\mathrm{hom} ⊗ α_{X_2 Y_2 Z_2}.\mathrm{hom})) = (α_{(X_1⊗X_2)(Y_1⊗Y_2)(Z_1⊗Z_2)}).\hom ≫ ((X_1⊗X_2) \triangleleft tensorμ Y_1 Y_2 Z_1 Z_2) ≫ tensorμ X_1 X_2 (Y_1 ⊗ Z_1) (Y_2 ⊗ Z_2).$$$$

Lean4

@[simp]
theorem tensor_δ (X Y : C × C) : δ (tensor C) X Y = tensorδ X.1 X.2 Y.1 Y.2 :=
  rfl

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