Documentation

TauCeti.Algebra.HopfAlgebra.InverseAntipode

The inverse of a bijective antipode #

For a Hopf algebra with explicitly supplied bijective antipode, inverseAntipode is its inverse linear map. It reverses multiplication, and its two inverse laws allow the contragredient actions through S and S⁻¹ to cancel on mixed double duals. No commutativity or star structure is assumed.

Bijectivity holds in particular when S² is an inner automorphism a ↦ g a g⁻¹ (antipode_bijective_of_antipode_antipode), as for the group-like element K⁻¹ of U_q(sl₂).

The construction uses Mathlib's LinearEquiv.ofBijective. See C. Kassel, Quantum Groups, Chapter III, for inverse-antipode duality.

source
theorem TauCeti.HopfAlgebra.antipode_bijective_of_antipode_antipode {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {g : Hˣ} (hg : ∀ (a : H), (HopfAlgebraStruct.antipode R) ((HopfAlgebraStruct.antipode R) a) = ↑g * a * ↑g⁻¹) :
Function.Bijective ⇑(HopfAlgebraStruct.antipode R)

If the square of the antipode is the inner automorphism a ↦ g a g⁻¹ of a unit g, then the antipode is bijective.

source
noncomputable def TauCeti.HopfAlgebra.inverseAntipode {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) :
H →ₗ[R] H

The inverse linear map of an explicitly bijective antipode.

Instances For
    source
    @[simp]
    theorem TauCeti.HopfAlgebra.antipode_inverseAntipode {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (a : H) :
    (HopfAlgebraStruct.antipode R) ((inverseAntipode hS) a) = a

    Applying the antipode after its inverse gives the original element.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.inverseAntipode_antipode {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (a : H) :
    (inverseAntipode hS) ((HopfAlgebraStruct.antipode R) a) = a

    Applying the inverse antipode after the antipode gives the original element.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.inverseAntipode_one {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) :
    (inverseAntipode hS) 1 = 1

    The inverse antipode preserves the unit.

    source
    theorem TauCeti.HopfAlgebra.inverseAntipode_mul {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (a b : H) :
    (inverseAntipode hS) (a * b) = (inverseAntipode hS) b * (inverseAntipode hS) a

    The inverse antipode reverses multiplication.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.inverseAntipode_algebraMap {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (r : R) :
    (inverseAntipode hS) ((algebraMap R H) r) = (algebraMap R H) r

    The inverse antipode fixes the scalar algebra map.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.mul_inverseAntipode_rTensor_comm_comul_apply {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (a : H) :
    (LinearMap.mul' R H) ((LinearMap.rTensor H (inverseAntipode hS)) ((TensorProduct.comm R H H) (CoalgebraStruct.comul a))) = (algebraMap R H) (CoalgebraStruct.counit a)

    The inverse antipode cancels the first leg of the reversed coproduct. This is the antipode identity used for evaluation of an inverse-antipode contragredient.

    source
    @[simp]
    theorem TauCeti.HopfAlgebra.mul_inverseAntipode_lTensor_comm_comul_apply {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (hS : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)) (a : H) :
    (LinearMap.mul' R H) ((LinearMap.lTensor H (inverseAntipode hS)) ((TensorProduct.comm R H H) (CoalgebraStruct.comul a))) = (algebraMap R H) (CoalgebraStruct.counit a)

    The inverse antipode cancels the second leg of the reversed coproduct. This is the antipode identity used for coevaluation of an inverse-antipode contragredient.