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