Comultiplication of the antipode

TheoremComultiplication of the antipode#✓fully proved

Comultiplication anticommutes with the antipode up to the tensor swap.

theorem HopfAlgebra.comul_antipode {R : Type*} [CommSemiring R]
    {A : Type*} [Semiring A] [HopfAlgebra R A] (a : A) :
    Coalgebra.comul (HopfAlgebra.antipode R a)
      = TensorProduct.comm R A A
          (TensorProduct.map (HopfAlgebra.antipode R) (HopfAlgebra.antipode R)
            (Coalgebra.comul a))

Used by 1

Used byComultiplication commutes with the antipode when cocommutative

TheoremComultiplication commutes with the antipode when cocommutative#✓fully proved

In a cocommutative Hopf algebra, comultiplication commutes with the antipode.

theorem HopfAlgebra.map_antipode_comul_of_isCocomm {R : Type*} [CommSemiring R]
    {A : Type*} [Semiring A] [HopfAlgebra R A] (hcocomm : Coalgebra.IsCocomm R A) (a : A) :
    TensorProduct.map (HopfAlgebra.antipode R) (HopfAlgebra.antipode R) (Coalgebra.comul a)
      = Coalgebra.comul (HopfAlgebra.antipode R a)

Uses 1

Proof usesComultiplication of the antipode

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.