Documentation

TauCeti.Algebra.HopfAlgebra.Antipode

Antipode identities for Hopf algebras #

The antipode of a Hopf algebra is an antihomomorphism for both its algebra and coalgebra structures. Mathlib already proves the multiplicative statement directly, as HopfAlgebra.antipode_mul_antidistrib. This file records the coalgebraic statement: applying the antipode before comultiplication is the same as comultiplying, swapping the two tensor factors, and applying the antipode to each factor.

For a commutative Hopf algebra, the antipode is involutive, hence defines an algebra automorphism. These facts are also recorded here in the commutative case.

Main declarations #

Implementation notes #

The proof of antipode_comul_antidistrib takes place in the convolution monoid of linear maps from the Hopf algebra to its tensor square. Comultiplication factors as the convolution product of the two canonical tensor inclusions, and postcomposing Mathlib's antipode convolution identity LinearMap.antipode_mul_id with those inclusions exhibits the proposed opposite comultiplication as a left inverse of comultiplication. Mathlib's LinearMap.comul_right_inv supplies the matching right inverse, so uniqueness of inverses finishes the proof.

The involutivity proof uses inv_inv in Mathlib's convolution group on algebra maps. The private lemma ofConv_inv isolates the single definitional unfolding of AlgHom.convInv needed to read that group identity as the pointwise equation S (S x) = x.

References #

The anti-coalgebra identity and involutivity in the commutative case are standard; see Sweedler, Hopf Algebras, Chapter 4, Proposition 4.0.1 for the anti-(co)algebra identity and Proposition 4.0.6 for involutivity. Mathlib formalizes these results for Hopf objects in a braided monoidal category as CategoryTheory.HopfObj.antipode_comul and CategoryTheory.HopfObj.antipode_antipode. The proofs below are ring-level analogues, stated for HopfAlgebra R C and HopfAlgebra R A so they apply directly to the bundled ring-theoretic antipode APIs.

source
@[simp]
theorem TauCeti.HopfAlgebra.antipode_antipode {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] (x : A) :
(HopfAlgebraStruct.antipode R) ((HopfAlgebraStruct.antipode R) x) = x

In a commutative Hopf algebra, applying the antipode twice is the identity.

source
noncomputable def TauCeti.HopfAlgebra.antipodeAlgEquiv {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] :
A ≃ₐ[R] A

The antipode of a commutative Hopf algebra as an involutive algebra equivalence.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipodeAlgEquiv_apply {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] (x : A) :
    antipodeAlgEquiv x = (HopfAlgebraStruct.antipode R) x

    The antipode algebra equivalence acts by the antipode.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipodeAlgEquiv_toAlgHom {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] :
    ↑antipodeAlgEquiv = HopfAlgebra.antipodeAlgHom R A

    The algebra homomorphism underlying the antipode equivalence is Mathlib's antipode algebra homomorphism.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipodeAlgEquiv_toRingHom {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] :
    ↑antipodeAlgEquiv = ↑(HopfAlgebra.antipodeAlgHom R A)

    The ring homomorphism underlying the antipode equivalence is Mathlib's antipode algebra homomorphism viewed as a ring homomorphism.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipodeAlgEquiv_symm {R : Type u} [CommSemiring R] {A : Type v} [CommSemiring A] [HopfAlgebra R A] :
    antipodeAlgEquiv.symm = antipodeAlgEquiv

    The antipode algebra equivalence is its own inverse.

    source
    theorem TauCeti.HopfAlgebra.antipode_comul_antidistrib {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :
    CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R = TensorProduct.map (HopfAlgebraStruct.antipode R) (HopfAlgebraStruct.antipode R) ∘ₗ ↑(TensorProduct.comm R C C) ∘ₗ CoalgebraStruct.comul

    The antipode reverses comultiplication: after comultiplication, swap the tensor factors and apply the antipode to each of them. This is the coalgebraic counterpart of HopfAlgebra.antipode_mul_antidistrib.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipode_comul_antidistrib_apply {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [HopfAlgebra R C] (c : C) :
    CoalgebraStruct.comul ((HopfAlgebraStruct.antipode R) c) = (TensorProduct.map (HopfAlgebraStruct.antipode R) (HopfAlgebraStruct.antipode R)) ((TensorProduct.comm R C C) (CoalgebraStruct.comul c))

    Pointwise form of antipode_comul_antidistrib.