Tensor products of bialgebras

We define the data in the monoidal structure on the category of bialgebras - e.g. the bialgebra instance on a tensor product of bialgebras, and the tensor product of two BialgHoms as a BialgHom. This is done by combining the corresponding API for coalgebras and algebras.

theorem Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : CoalgebraStruct.counit = ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap

theorem Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : CoalgebraStruct.comul = ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap

noncomputable instance TensorProduct.instBialgebra (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : Bialgebra S (TensorProduct R A B)

noncomputable def Bialgebra.TensorProduct.map {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) : TensorProduct R A B →ₐc[S] TensorProduct R C D

The tensor product of two bialgebra morphisms as a bialgebra morphism.

@[simp]

theorem Bialgebra.TensorProduct.map_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) (x : A) (y : B) : (map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

@[simp]

theorem Bialgebra.TensorProduct.map_toCoalgHom {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) : ↑(map f g) = Coalgebra.TensorProduct.map ↑f ↑g

@[simp]

theorem Bialgebra.TensorProduct.map_toAlgHom {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) : ↑(map f g) = Algebra.TensorProduct.map ↑f ↑g

noncomputable def Bialgebra.TensorProduct.assoc (R : Type u_1) (S : Type u_2) (A : Type u_3) (C : Type u_5) (D : Type u_6) [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] : TensorProduct R (TensorProduct S A C) D ≃ₐc[S] TensorProduct S A (TensorProduct R C D)

The associator for tensor products of R-bialgebras, as a bialgebra equivalence.

@[simp]

theorem Bialgebra.TensorProduct.assoc_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (x : A) (y : C) (z : D) : (TensorProduct.assoc R S A C D) (x ⊗ₜ[S] y ⊗ₜ[R] z) = x ⊗ₜ[S] (y ⊗ₜ[R] z)

@[simp]

theorem Bialgebra.TensorProduct.assoc_symm_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] (x : A) (y : C) (z : D) : (TensorProduct.assoc R S A C D).symm (x ⊗ₜ[S] (y ⊗ₜ[R] z)) = x ⊗ₜ[S] y ⊗ₜ[R] z

@[simp]

theorem Bialgebra.TensorProduct.assoc_toCoalgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] : ↑(TensorProduct.assoc R S A C D) = Coalgebra.TensorProduct.assoc R S A C D

@[simp]

theorem Bialgebra.TensorProduct.assoc_toAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] [Semiring C] [Semiring D] [Bialgebra S C] [Bialgebra R D] [Algebra R C] [IsScalarTower R S C] : ↑(TensorProduct.assoc R S A C D) = Algebra.TensorProduct.assoc R S A C D

noncomputable def Bialgebra.TensorProduct.lid (R : Type u_1) (B : Type u_4) [CommSemiring R] [Semiring B] [Bialgebra R B] : TensorProduct R R B ≃ₐc[R] B

The base ring is a left identity for the tensor product of bialgebras, up to bialgebra equivalence.

@[simp]

theorem Bialgebra.TensorProduct.lid_toCoalgEquiv {R : Type u_1} {B : Type u_4} [CommSemiring R] [Semiring B] [Bialgebra R B] : ↑(TensorProduct.lid R B) = Coalgebra.TensorProduct.lid R B

@[simp]

theorem Bialgebra.TensorProduct.lid_toAlgEquiv {R : Type u_1} {B : Type u_4} [CommSemiring R] [Semiring B] [Bialgebra R B] : ↑(TensorProduct.lid R B) = Algebra.TensorProduct.lid R B

@[simp]

theorem Bialgebra.TensorProduct.lid_tmul {R : Type u_1} {B : Type u_4} [CommSemiring R] [Semiring B] [Bialgebra R B] (r : R) (a : B) : (TensorProduct.lid R B) (r ⊗ₜ[R] a) = r • a

@[simp]

theorem Bialgebra.TensorProduct.lid_symm_apply {R : Type u_1} {B : Type u_4} [CommSemiring R] [Semiring B] [Bialgebra R B] (a : B) : (TensorProduct.lid R B).symm a = 1 ⊗ₜ[R] a

theorem Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] (x : TensorProduct R A R) : (Coalgebra.TensorProduct.rid R S A) x = (Algebra.TensorProduct.rid R R A) x

noncomputable def Bialgebra.TensorProduct.rid (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : TensorProduct R A R ≃ₐc[S] A

The base ring is a right identity for the tensor product of bialgebras, up to bialgebra equivalence.

@[simp]

theorem Bialgebra.TensorProduct.rid_toCoalgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : ↑(TensorProduct.rid R S A) = Coalgebra.TensorProduct.rid R S A

@[simp]

theorem Bialgebra.TensorProduct.rid_toAlgEquiv {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : ↑(TensorProduct.rid R S A) = Algebra.TensorProduct.rid R S A

@[simp]

theorem Bialgebra.TensorProduct.rid_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] (r : R) (a : A) : (TensorProduct.rid R S A) (a ⊗ₜ[R] r) = r • a

@[simp]

theorem Bialgebra.TensorProduct.rid_symm_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Bialgebra S A] [Algebra R A] [Algebra R S] [IsScalarTower R S A] (a : A) : (TensorProduct.rid R S A).symm a = a ⊗ₜ[R] 1

@[reducible, inline]

noncomputable abbrev BialgHom.lTensor {R : Type u_1} (A : Type u_2) {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] (f : B →ₐc[R] C) : TensorProduct R A B →ₐc[R] TensorProduct R A C

lTensor A f : A ⊗ B →ₐc A ⊗ C is the natural bialgebra morphism induced by f : B →ₐc C.

@[reducible, inline]

noncomputable abbrev BialgHom.rTensor {R : Type u_1} (A : Type u_2) {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] (f : B →ₐc[R] C) : TensorProduct R B A →ₐc[R] TensorProduct R C A

rTensor A f : B ⊗ A →ₐc C ⊗ A is the natural bialgebra morphism induced by f : B →ₐc C.