English
A detailed auxiliary identity showing interaction of μ and 𝒮 via associator/naturality and braiding steps.
Русский
Подробная вспомогательная идентичность, показывающая взаимодействие μ и 𝒮 через ассоциатор и браидинг.
LaTeX
$$$ (Δ_A ⊗ Δ_A) ≫ (α_{A A (A⊗A)})^{hom} ≫ A ◁ (α_{A A A})^{inv} ≫ A ◁ (β_{A A})^{hom} ≫ (α_{A(A⊗A)A})^{inv} ≫ (α_{A A A})^{inv} ▷ A ≫ μ_A ▷ A ▷ A ≫ 𝒮_A ▷ A ▷ A ≫ (α_{A A A})^{hom} ≫ A ◁ μ_A ≫ μ_A = (ε_A ⊗ ε_A) ≫ λ_I^{hom} η_A$$
Lean4
/-- Auxiliary calculation for `antipode_comul`.
This calculation calls for some ASCII art out of This Week's Finds.
```
| |
n n
| \ / |
| / |
| / \ |
| | S S
| | \ /
| | /
| | / \
\ / \ /
v v
\ /
v
|
```
We move the left antipode up through the crossing,
the right antipode down through the crossing,
the right multiplication down across the strand,
reassociate the comultiplications,
then use `antipode_right` then `antipode_left` to simplify.
-/
theorem antipode_comul₂ (A : C) [HopfObj A] :
Δ[A] ≫
Δ[A] ▷ A ≫
(α_ A A A).hom ≫
A ◁ A ◁ Δ[A] ≫
A ◁ A ◁ (β_ A A).hom ≫
A ◁ A ◁ (𝒮[A] ⊗ₘ 𝒮[A]) ≫
A ◁ (α_ A A A).inv ≫
A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv ≫ (μ[A] ⊗ₘ μ[A]) =
ε[A] ≫ (λ_ (𝟙_ C)).inv ≫ (η[A] ⊗ₘ η[A]) :=
by
-- We should write a version of `slice_lhs` that zooms through whiskerings.
slice_lhs 6 6 => simp only [tensorHom_def', whiskerLeft_comp]
slice_lhs 7 8 => rw [← whiskerLeft_comp, associator_inv_naturality_middle, whiskerLeft_comp]
slice_lhs 8 9 =>
rw [← whiskerLeft_comp, ← comp_whiskerRight, BraidedCategory.braiding_naturality_right, comp_whiskerRight,
whiskerLeft_comp]
slice_lhs 9 10 => rw [← whiskerLeft_comp, associator_naturality_left, whiskerLeft_comp]
slice_lhs 5 6 =>
rw [← whiskerLeft_comp, ← whiskerLeft_comp, ← BraidedCategory.braiding_naturality_left, whiskerLeft_comp,
whiskerLeft_comp]
slice_lhs 11 12 => rw [tensorHom_def', ← Category.assoc, ← associator_inv_naturality_right]
slice_lhs 10 11 => rw [← whiskerLeft_comp, ← whisker_exchange, whiskerLeft_comp]
slice_lhs 6 10 =>
simp only [← whiskerLeft_comp]
rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc, ← BraidedCategory.braiding_naturality_left]
simp only [whiskerLeft_comp]
rw [ComonObj.comul_assoc_flip_assoc, Iso.inv_hom_id_assoc]
slice_lhs 2 3 =>
simp only [← whiskerLeft_comp]
rw [ComonObj.comul_assoc]
simp only [whiskerLeft_comp]
slice_lhs 3 7 =>
simp only [← whiskerLeft_comp]
rw [← associator_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 2 3 =>
simp only [← whiskerLeft_comp]
rw [ComonObj.counit_comul]
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 [whisker_exchange]
simp only [whiskerLeft_comp]
slice_lhs 5 7 => rw [associator_inv_naturality_right_assoc, whisker_exchange]
simp only [braiding_tensorUnit_left, whiskerLeft_comp, whiskerLeft_rightUnitor_inv, whiskerRight_id,
whiskerLeft_rightUnitor, Category.assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, whiskerLeft_inv_hom_assoc,
antipode_right_assoc]
rw [rightUnitor_inv_naturality_assoc, tensorHom_def]
monoidal
