pentagon — Mathlib

English

The associator coherence condition (pentagon) holds for the chosen finite products; the two different ways of re-associating a triple tensor product give the same morphism.

Русский

Когерентость ассоциатора (пентагон) выполняется для выбранных конечных произведений; два способа перестановки трёхтензорных произведений совпадают по морфизму.

LaTeX

$$$$ (associator) \_W X Y \to ... $$$$

Lean4

theorem pentagon (W X Y Z : C) :
    tensorHom ℬ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom (𝟙 Z) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          tensorHom ℬ (𝟙 W) (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom =
      (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom :=
  by
  dsimp [tensorHom]
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩ <;> simp

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