Multiplicativity of the BCK Antipode

The antipode of the commutative BCK Hopf algebra is an algebra morphism: S(φψ) = S(φ)S(ψ). The proof is by strong induction on total order, using the convolution identity μ(S ⊗ I)Δ = u ∘ e: expanding μ(S ⊗ I)Δ(φψ) over products of coproduct terms and comparing with (μ(S ⊗ I)Δφ)(μ(S ⊗ I)Δψ) = 0, every paired term agrees by the induction hypothesis except the unique full-cut pair, whose difference is exactly S(φψ) - S(φ)S(ψ).

Main definitions

• RootedForest.antipode_add - multiplicativity on forest monomials
• ForestAlgebra.antipode_mul - multiplicativity on the whole algebra
• ForestAlgebra.antipodeAlgHom - the antipode as an algebra homomorphism

theorem HopfAlgebras.RootedForest.coproductTerms_filterMap_rightBoundary (φ : RootedForest) : List.filterMap PTree.rightBoundaryCoproductTerm? φ.coproductTerms = [(φ, 0)]

The forest coproduct has exactly one term with empty right factor, namely the full cut φ ⊗ 1.

theorem HopfAlgebras.RootedForest.self_zero_mem_coproductTerms (φ : RootedForest) : (φ, 0) ∈ φ.coproductTerms

The full cut is a coproduct term of every forest.

theorem HopfAlgebras.RootedForest.antipode_add {R : Type u} [CommRing R] (φ ψ : RootedForest) : (φ + ψ).antipode = φ.antipode * ψ.antipode

The BCK antipode is multiplicative on forest monomials: S(φψ) = S(φ)S(ψ).

theorem HopfAlgebras.RootedForest.order_eq_of_mem_support_antipode {R : Type u} [CommRing R] {φ ψ : RootedForest} (hψ : ψ ∈ φ.antipode.support) : ψ.order = φ.order

The BCK antipode preserves the order grading: S(φ) is supported on forests of the same order as φ.

theorem HopfAlgebras.ForestAlgebra.antipode_one {R : Type u} [CommRing R] : antipode 1 = 1

The linear antipode preserves the unit.

theorem HopfAlgebras.ForestAlgebra.antipode_mul {R : Type u} [CommRing R] (x y : ForestAlgebra R) : antipode (x * y) = antipode x * antipode y

The BCK antipode is an algebra morphism, since the BCK Hopf algebra is commutative.

noncomputable def HopfAlgebras.ForestAlgebra.antipodeAlgHom (R : Type u) [CommRing R] : ForestAlgebra R →ₐ[R] ForestAlgebra R

The BCK antipode as an algebra homomorphism.

Equations

• HopfAlgebras.ForestAlgebra.antipodeAlgHom R = AlgHom.ofLinearMap HopfAlgebras.ForestAlgebra.antipode ⋯ ⋯

@[simp]

theorem HopfAlgebras.ForestAlgebra.antipodeAlgHom_apply {R : Type u} [CommRing R] (x : ForestAlgebra R) : (antipodeAlgHom R) x = antipode x