antipode_comul — Mathlib

English

A second auxiliary identity aligning μ and 𝒮 through associators and braidings.

Русский

Вторая вспомогательная идентичность, сопоставляющая μ и 𝒮 через ассоциаторы и браидинг.

LaTeX

$$$ (Δ_A ⊗ Δ_A) ≫ (α_{A A (A⊗A)})^{inv} ≫ (μ_A ∘ 𝒮_A) ≈ (ε_A ⊗ ε_A) ≫ η_A $$$

Lean4

theorem antipode_comul (A : C) [HopfObj A] : 𝒮[A] ≫ Δ[A] = Δ[A] ≫ (β_ _ _).hom ≫ (𝒮[A] ⊗ₘ 𝒮[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])
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, tensor_whiskerLeft, MonObj.tensorObj.mul_def, Category.assoc,
      MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₁ A
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [whiskerLeft_comp, tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc, MonObj.tensorObj.mul_def,
      MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₂ A

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