Tensor products of Hopf algebras #
We define the Hopf algebra instance on the tensor product of two Hopf algebras.
@[reducible, inline]
noncomputable abbrev
HopfAlgebra.ofAlgHom
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[CommSemiring A]
[Bialgebra R A]
(antipode : A →ₐ[R] A)
(mul_antipode_rTensor_comul :
(Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A))
(mul_antipode_lTensor_comul :
(Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A))
:
HopfAlgebra R A
Upgrade a bialgebra to a Hopf algebra by specifying the antipode as an algebra map with appropriate conditions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
TensorProduct.instHopfAlgebra
{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]
:
HopfAlgebra S (TensorProduct R B A)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
TensorProduct.antipode_def
{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]
: