English
Two long braid-convolution identities express the interaction of antipode with comultiplication in a Hopf object.
Русский
Две детализированные идентичности конволюции выражают взаимодействие antipode с комуляцией в Hopf-объекте.
LaTeX
$$$ Δ_A ≫ 𝒮_A ▷ A ≫ Δ_A ▷ A ≫ (α_{A,A,A})^{hom} ≫ 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 ≫ λ_{I}^{-1} ≫ (η_A ⊗ η_A) $$$
Lean4
/-- Morphisms of Hopf monoids intertwine the antipodes. -/
theorem hom_antipode {A B : C} [HopfObj A] [HopfObj B] (f : A ⟶ B) [IsBimonHom f] : f ≫ 𝒮 = 𝒮 ≫ f := by
-- We show these elements are equal by exhibiting an element in the convolution algebra
-- between `A` (as a comonoid) and `B` (as a monoid),
-- such that the LHS is a left inverse, and the RHS is a right inverse.
apply left_inv_eq_right_inv (M := Conv A B) (a := f)
· rw [Conv.mul_eq, Conv.one_eq]
simp only [comp_whiskerRight, Category.assoc]
slice_lhs 3 4 => rw [← whisker_exchange]
slice_lhs 2 3 => rw [← tensorHom_def]
slice_lhs 1 2 => rw [← IsComonHom.hom_comul f]
slice_lhs 2 4 => rw [antipode_left]
slice_lhs 1 2 => rw [IsComonHom.hom_counit]
· rw [Conv.mul_eq, Conv.one_eq]
simp only [whiskerLeft_comp, Category.assoc]
slice_lhs 2 3 => rw [← whisker_exchange]
slice_lhs 3 4 => rw [← tensorHom_def]
slice_lhs 3 4 => rw [← IsMonHom.mul_hom]
slice_lhs 1 3 => rw [antipode_right]
slice_lhs 2 3 => rw [IsMonHom.one_hom]
