Antipode properties and a bialgebra convolution-power criterion

TheoremAntipode of a commutative Hopf algebra is an involution#✓fully proved

The antipode of a commutative Hopf algebra is an involution.

theorem HopfAlgebra.antipode_antipode {R : Type*} [CommSemiring R]
    {A : Type*} [CommSemiring A] [HopfAlgebra R A] (a : A) :
    HopfAlgebra.antipode R (HopfAlgebra.antipode R a) = a

TheoremAlgebra homomorphisms from a Hopf algebra are convolution units#✓fully proved

Algebra homomorphisms from a possibly noncommutative Hopf algebra to a commutative algebra are convolution units.

theorem HopfAlgebra.isUnit_withConv_algHom {R : Type*} [CommSemiring R]
    {A : Type*} [Semiring A] [HopfAlgebra R A]
    {L : Type*} [CommSemiring L] [Algebra R L]
    (φ : WithConv (A →ₐ[R] L)) : IsUnit φ

TheoremConvolution inverse of an algebra homomorphism via the antipode#✓fully proved

Every algebra homomorphism from a possibly noncommutative Hopf algebra to a commutative algebra has a convolution inverse given by precomposition with the antipode.

theorem HopfAlgebra.exists_comp_antipode_convMul_eq_one
    {K : Type*} [CommSemiring K] {A : Type*} [Semiring A] [HopfAlgebra K A]
    {L : Type*} [CommSemiring L] [Algebra K L] (ν : A →ₐ[K] L) :
    ∃ ν' : A →ₐ[K] L,
      ν'.toLinearMap = ν.toLinearMap ∘ₗ HopfAlgebraStruct.antipode (R := K) ∧
      WithConv.toConv ν' * WithConv.toConv ν = 1 ∧
      WithConv.toConv ν * WithConv.toConv ν' = 1

TheoremConvolution-power criterion for bialgebras#✓fully proved

A convolution power is trivial on all points iff it is trivial on the universal point.

theorem Bialgebra.forall_withConv_pow_eq_one_iff_toConv_id_pow_eq_one
    {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [Bialgebra R H] (m : ℕ) :
    (∀ (T : Type v) [CommSemiring T] [Algebra R T] (f : WithConv (H →ₐ[R] T)), f ^ m = 1) ↔
      (WithConv.toConv (AlgHom.id R H)) ^ m = 1

Used by 1

Used byConvolution-power criterion for Hopf algebras

TheoremConvolution-power criterion for Hopf algebras#✓fully proved

A compatibility corollary for the convolution-power criterion on Hopf algebras.

theorem HopfAlgebra.forall_withConv_pow_eq_one_iff_toConv_id_pow_eq_one
    {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (m : ℕ) :
    (∀ (T : Type v) [CommRing T] [Algebra R T] (f : WithConv (H →ₐ[R] T)), f ^ m = 1) ↔
      (WithConv.toConv (AlgHom.id R H)) ^ m = 1

Uses 1

Proof usesConvolution-power criterion for bialgebras

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.