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

@[implicit_reducible]

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)

Equations

• TensorProduct.instBialgebra R S A B = Bialgebra.mk' S (TensorProduct R A B) ⋯ ⋯ ⋯ ⋯

theorem Bialgebra.TensorProduct.counitAlgHom_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] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : counitAlgHom S (TensorProduct R A B) = (↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))

theorem Bialgebra.TensorProduct.comulAlgHom_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] [Bialgebra S A] [Bialgebra R B] [Algebra R A] [Algebra R S] [IsScalarTower R S A] : comulAlgHom S (TensorProduct R A B) = (↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R 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.

Equations

• Bialgebra.TensorProduct.map f g = { toCoalgHom := Coalgebra.TensorProduct.map ↑f ↑g, map_one' := ⋯, map_mul' := ⋯ }

@[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.

Equations

• Bialgebra.TensorProduct.assoc R S A C D = { toCoalgEquiv := Coalgebra.TensorProduct.assoc R S A C D, map_mul' := ⋯ }

@[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).toAlgEquiv = Algebra.TensorProduct.assoc R S 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.

Equations

• Bialgebra.TensorProduct.lid R B = { toCoalgEquiv := Coalgebra.TensorProduct.lid R B, map_mul' := ⋯ }

@[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).toAlgEquiv = 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.

Equations

• Bialgebra.TensorProduct.rid R S A = { toCoalgEquiv := Coalgebra.TensorProduct.rid R S A, map_mul' := ⋯ }

@[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).toAlgEquiv = 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

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

The tensor product of R-bialgebras is commutative, up to bialgebra isomorphism.

Equations

• Bialgebra.TensorProduct.comm R A B = BialgEquiv.ofAlgEquiv (Algebra.TensorProduct.comm R A B) ⋯ ⋯

@[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.

Equations

• BialgHom.lTensor A f = Bialgebra.TensorProduct.map (BialgHom.id R A) f

@[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.

Equations

• BialgHom.rTensor A f = Bialgebra.TensorProduct.map f (BialgHom.id R A)

noncomputable def Bialgebra.comulBialgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] [Coalgebra.IsCocomm R A] : A →ₐc[R] TensorProduct R A A

Comultiplication as a bialgebra hom.

Equations

• Bialgebra.comulBialgHom R A = { toFun := (↑↑(Bialgebra.comulAlgHom R A).toRingHom).toFun, map_add' := ⋯, map_smul' := ⋯, counit_comp := ⋯, map_comp_comul := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Bialgebra.comm_comp_comulBialgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] [Coalgebra.IsCocomm R A] : (TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A) = comulBialgHom R A

def Bialgebra.mulCoalgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] : TensorProduct R A A →ₗc[R] A

Multiplication on a bialgebra as a coalgebra hom.

Equations

• Bialgebra.mulCoalgHom R A = { toLinearMap := LinearMap.mul' R A, counit_comp := ⋯, map_comp_comul := ⋯ }

@[simp]

theorem Bialgebra.toLinearMap_mulCoalgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : ↑(mulCoalgHom R A) = LinearMap.mul' R A

@[simp]

theorem Bialgebra.coe_mulCoalgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : ⇑(mulCoalgHom R A) = ⇑(LinearMap.mul' R A)

def Bialgebra.mulBialgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Bialgebra R A] : TensorProduct R A A →ₐc[R] A

Multiplication on a commutative bialgebra as a bialgebra hom.

Equations

• Bialgebra.mulBialgHom R A = { toCoalgHom := Bialgebra.mulCoalgHom R A, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Bialgebra.mulBialgHom_toCoalgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Bialgebra R A] : (mulBialgHom R A).toCoalgHom = mulCoalgHom R A

@[simp]

theorem Bialgebra.mulBialgHom_toAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] : ↑(mulBialgHom R A) = Algebra.TensorProduct.lmul' R

@[simp]

theorem Bialgebra.coe_mulBialgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] : ⇑(mulBialgHom R A) = ⇑(LinearMap.mul' R A)