mul_antipode — Mathlib

English

The multiplication and antipode satisfy a compatibility: μ_A ≫ 𝒮_A = (𝒮_A ⊗ 𝒮_A) ≫ (β_{_,_})^hom ≫ μ_A.

Русский

совместимость умножения и antipode.

LaTeX

$$$ μ_A ≫ 𝒮_A = (𝒮_A \otimes 𝒮_A) \circ (β_{A,A})^{\mathrm{hom}} \circ μ_A $$$

Lean4

theorem mul_antipode (A : C) [HopfObj A] : μ[A] ≫ 𝒮[A] = (𝒮[A] ⊗ₘ 𝒮[A]) ≫ (β_ _ _).hom ≫ μ[A] := by
  -- Again, it is a "left inverse equals right inverse" argument in the convolution monoid.

  apply left_inv_eq_right_inv (M := Conv (A ⊗ A) A) (a := μ[A])
  · -- Unfold the algebra structure in the convolution monoid,
        -- then `simp?, simp only [tensor_μ], simp?`.

    rw [Conv.mul_eq, Conv.one_eq]
    simp only [Comon.tensorObj_comul, whiskerRight_tensor, comp_whiskerRight, Category.assoc, Comon.tensorObj_counit]
    simp only [tensorμ]
    simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]
    exact mul_antipode₁ A
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [Comon.tensorObj_comul, whiskerRight_tensor, BraidedCategory.braiding_naturality_assoc, whiskerLeft_comp,
      Category.assoc, Comon.tensorObj_counit]
    simp only [tensorμ]
    simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]
    exact mul_antipode₂ A

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