Documentation

TauCeti.Algebra.HopfAlgebra.Basic

Hopf algebra morphisms #

This file records Hopf-algebra API needed for the affine-group-scheme dictionary in the reductive-groups roadmap. Mathlib defines morphisms in HopfAlgCat R to be bialgebra morphisms; the missing algebraic fact is that such a morphism automatically preserves the antipode. We prove that here by the usual convolution-inverse uniqueness argument.

Main results #

References #

This supplies a formal prerequisite for the Tau Ceti reductive-groups roadmap, Layer 0, "the functor of points and the three-way dictionary": morphisms in the Hopf-algebra model must respect the inverse map in the affine group-scheme model. The proof uses Mathlib's convolution product on linear maps, due to Yaël Dillies, Michał Mrugała and Yunzhou Xie. The tensor-product antipode formula uses Mathlib's Mathlib.RingTheory.HopfAlgebra.TensorProduct, specifically TensorProduct.antipode_def.

source
@[simp]
theorem TauCeti.TensorProduct.antipode_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [HopfAlgebra R A] [HopfAlgebra S B] [Algebra R B] [IsScalarTower R S B] (b : B) (a : A) :
(HopfAlgebraStruct.antipode S) (b ⊗ₜ[R] a) = (HopfAlgebraStruct.antipode S) b ⊗ₜ[R] (HopfAlgebraStruct.antipode R) a

The antipode on a tensor product of Hopf algebras acts componentwise on pure tensors.

source
@[simp]
theorem TauCeti.HopfAlgebra.baseChange_antipode_tmul {k : Type u_3} {K : Type u_4} {A : Type u_5} [CommSemiring k] [CommSemiring K] [Semiring A] [Algebra k K] [HopfAlgebra k A] (s : K) (a : A) :
(HopfAlgebraStruct.antipode K) (s ⊗ₜ[k] a) = s ⊗ₜ[k] (HopfAlgebraStruct.antipode k) a

The antipode on the base-changed Hopf algebra K ⊗[k] A sends a pure tensor s ⊗ a to s ⊗ S a.

source
theorem TauCeti.HopfAlgebra.antipode_convMul_id {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] :
WithConv.toConv (HopfAlgebraStruct.antipode R) * WithConv.toConv LinearMap.id = 1

The antipode is a left convolution inverse of the identity in the convolution ring of linear maps: S * id = 1. This is a restatement of the antipode axiom HopfAlgebra.mul_antipode_rTensor_comul.

source
theorem TauCeti.HopfAlgebra.id_convMul_antipode {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [HopfAlgebra R H] :
WithConv.toConv LinearMap.id * WithConv.toConv (HopfAlgebraStruct.antipode R) = 1

The antipode is a right convolution inverse of the identity in the convolution ring of linear maps: id * S = 1. This is a restatement of the antipode axiom HopfAlgebra.mul_antipode_lTensor_comul.

source
theorem TauCeti.BialgHom.toLinearMap_comp_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] (φ : A →ₐc[R] B) :
φ.toLinearMap ∘ₗ HopfAlgebraStruct.antipode R = HopfAlgebraStruct.antipode R ∘ₗ φ.toLinearMap

A bialgebra morphism between Hopf algebras commutes with the antipodes, as a statement about underlying linear maps.

source
theorem TauCeti.BialgHom.map_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] (φ : A →ₐc[R] B) (a : A) :
φ ((HopfAlgebraStruct.antipode R) a) = (HopfAlgebraStruct.antipode R) (φ a)

A bialgebra morphism between Hopf algebras commutes with the antipodes, pointwise.

source
@[simp]
theorem TauCeti.BialgHomClass.map_antipode {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebra R B] [FunLike F A B] [BialgHomClass F R A B] (φ : F) (a : A) :
φ ((HopfAlgebraStruct.antipode R) a) = (HopfAlgebraStruct.antipode R) (φ a)

A bialgebra-hom-like map between Hopf algebras commutes with the antipodes, pointwise.