English
A Yang–Baxter identity is satisfied by the braiding in braided monoidal categories, giving a coherent braid relation.
Русский
Уравнение Ян–Баксера выполняется для переплетения в связанной монодальной категории, обеспечивая когерентное отношение и braid.
LaTeX
$$$\\text{yang\_baxter\_iso}(X,Y,Z)$$$
Lean4
/-- Auxiliary calculation for `mul_antipode`.
```
|
n
/ \
| n
| / \
| S S
| \ /
n /
/ \ / \
| / |
\ / \ /
v v
| |
```
We move the leftmost multiplication up, so we can reassociate.
We then move the rightmost comultiplication under the strand,
and simplify using `antipode_right`.
-/
theorem mul_antipode₂ (A : C) [HopfObj A] :
(Δ[A] ⊗ₘ Δ[A]) ≫
(α_ A A (A ⊗ A)).hom ≫
A ◁ (α_ A A A).inv ≫
A ◁ (β_ A A).hom ▷ A ≫
(α_ A (A ⊗ A) A).inv ≫
(α_ A A A).inv ▷ A ≫
μ[A] ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮[A] ⊗ₘ 𝒮[A]) ≫ A ◁ μ[A] ≫ μ[A] =
(ε[A] ⊗ₘ ε[A]) ≫ (λ_ (𝟙_ C)).hom ≫ η[A] :=
by
slice_lhs 7 8 => rw [associator_naturality_left]
slice_lhs 8 9 => rw [← whisker_exchange]
slice_lhs 9 10 => rw [← whisker_exchange]
slice_lhs 11 12 => rw [MonObj.mul_assoc_flip]
slice_lhs 10 11 => rw [associator_inv_naturality_left]
slice_lhs 11 12 =>
simp only [← comp_whiskerRight]
rw [MonObj.mul_assoc]
simp only [comp_whiskerRight]
rw [tensorHom_def]
rw [tensor_whiskerLeft _ _ (β_ A A).hom]
rw [pentagon_inv_inv_hom_hom_inv_assoc]
slice_lhs 7 8 => rw [Iso.inv_hom_id]
rw [Category.id_comp]
slice_lhs 5 7 =>
simp only [← whiskerLeft_comp]
rw [← BraidedCategory.hexagon_forward]
simp only [whiskerLeft_comp]
simp only [tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc, pentagon_inv_inv_hom_inv_inv, whisker_assoc,
MonObj.mul_assoc, whiskerLeft_inv_hom_assoc]
slice_lhs 3 4 =>
simp only [← whiskerLeft_comp]
rw [BraidedCategory.braiding_naturality_right]
simp only [whiskerLeft_comp]
rw [tensorHom_def']
simp only [whiskerLeft_comp]
slice_lhs 5 6 =>
simp only [← whiskerLeft_comp]
rw [← associator_naturality_right]
simp only [whiskerLeft_comp]
slice_lhs 4 5 =>
simp only [← whiskerLeft_comp]
rw [← whisker_exchange]
simp only [whiskerLeft_comp]
slice_lhs 5 9 =>
simp only [← whiskerLeft_comp]
rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
simp only [← comp_whiskerRight]
rw [antipode_right]
simp only [comp_whiskerRight]
simp only [whiskerLeft_comp]
slice_lhs 6 7 =>
simp only [← whiskerLeft_comp]
rw [MonObj.one_mul]
simp only [whiskerLeft_comp]
slice_lhs 3 4 =>
simp only [← whiskerLeft_comp]
rw [← BraidedCategory.braiding_naturality_left]
simp only [whiskerLeft_comp]
slice_lhs 4 5 =>
simp only [← whiskerLeft_comp]
rw [← BraidedCategory.braiding_naturality_right]
simp only [whiskerLeft_comp]
rw [← associator_naturality_middle_assoc]
simp only [braiding_tensorUnit_right, whiskerLeft_comp]
slice_lhs 6 7 =>
simp only [← whiskerLeft_comp]
rw [Iso.inv_hom_id]
simp only [whiskerLeft_comp]
simp only [whiskerLeft_id, Category.id_comp]
slice_lhs 5 6 => rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
rw [associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc]
slice_lhs 3 4 => rw [whisker_exchange]
slice_lhs 1 3 =>
simp only [← comp_whiskerRight]
rw [antipode_right]
simp only [comp_whiskerRight]
slice_lhs 2 3 => rw [← whisker_exchange]
slice_lhs 1 2 =>
dsimp
rw [← tensorHom_def]
slice_lhs 2 3 => rw [rightUnitor_naturality]
monoidal
