associator_naturality — Mathlib

English

The pentagon identity for the associator holds for graded objects, expressing coherence of quadruple tensor products via the associator morphisms.

Русский

Пентагональная тождественность для ассоциатора для градуированных объектов, выражающая когерентность тензорных произведений четырех объектов через морфизмы ассоциатора.

LaTeX

$$$\text{pentagon } = \text{(complicated equality of tensor associators in the graded setting)}$$$

Lean4

theorem associator_naturality (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) [HasGoodTensor₁₂Tensor X₁ X₂ X₃]
    [HasGoodTensorTensor₂₃ X₁ X₂ X₃] [HasGoodTensor₁₂Tensor Y₁ Y₂ Y₃] [HasGoodTensorTensor₂₃ Y₁ Y₂ Y₃] :
    tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) :=
  by cat_disch

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