Tensor products of Hopf algebras #
We define the Hopf algebra instance on the tensor product of two Hopf algebras.
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]
: