English
The interaction of tensor and Braided category structures yields a family of coherence identities, including the pentagon and hexagon relations, for all tensorings of multiple objects.
Русский
Взаимодействие тензорной и браидированной структур приводит к набору когерентных тождеств, включая пентагон и гексагон, для тензорирования нескольких объектов.
LaTeX
$$$$ \text{Pentagon} \quad \text{and} \quad \text{Hexagon} \quad \text{coherence identities hold for all objects.} $$$$
Lean4
@[reassoc]
theorem tensor_left_unitality (X₁ X₂ : C) :
(λ_ (X₁ ⊗ X₂)).hom = ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫ tensorμ (𝟙_ C) (𝟙_ C) X₁ X₂ ≫ ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom) :=
by
dsimp only [tensorμ]
have :
((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ :=
by simp
slice_rhs 1 3 => rw [this]
clear this
slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight, leftUnitor_inv_braiding]
simp [tensorHom_def]
