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.

Implementation notes

Since the coalgebra instance on a tensor product of coalgebras is defined using a universe monomorphic monoidal category structure on ModuleCat R, we require our bialgebras to be in the same universe as the base ring R here too. Any contribution that achieves universe polymorphism would be welcome. For instance, the tensor product of bialgebras in the FLT repo is already universe polymorphic since it does not go via category theory.

theorem Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [Ring A] [Ring B] [Bialgebra R A] [Bialgebra R B] : Coalgebra.counit = ((Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map (Bialgebra.counitAlgHom R A) (Bialgebra.counitAlgHom R B))).toLinearMap

theorem Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [Ring A] [Ring B] [Bialgebra R A] [Bialgebra R B] : Coalgebra.comul = ((↑(Algebra.TensorProduct.tensorTensorTensorComm R A A B B)).comp (Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A) (Bialgebra.comulAlgHom R B))).toLinearMap

noncomputable instance TensorProduct.instBialgebra {R A B : Type u} [CommRing R] [Ring A] [Ring B] [Bialgebra R A] [Bialgebra R B] : Bialgebra R (TensorProduct R A B)

Equations

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

noncomputable def Bialgebra.TensorProduct.map {R A B C D : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] [Bialgebra R D] (f : A →ₐc[R] B) (g : C →ₐc[R] D) : TensorProduct R A C →ₐc[R] TensorProduct R B 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 A B C D : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] [Bialgebra R D] (f : A →ₐc[R] B) (g : C →ₐc[R] D) (x : A) (y : C) : (Bialgebra.TensorProduct.map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

@[simp]

theorem Bialgebra.TensorProduct.map_toCoalgHom {R A B C D : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] [Bialgebra R D] (f : A →ₐc[R] B) (g : C →ₐc[R] D) : ↑(Bialgebra.TensorProduct.map f g) = Coalgebra.TensorProduct.map ↑f ↑g

@[simp]

theorem Bialgebra.TensorProduct.map_toAlgHom {R A B C D : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Ring D] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] [Bialgebra R D] (f : A →ₐc[R] B) (g : C →ₐc[R] D) : ↑(Bialgebra.TensorProduct.map f g) = Algebra.TensorProduct.map ↑f ↑g

noncomputable def Bialgebra.TensorProduct.assoc (R A B C : Type u) [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] : TensorProduct R (TensorProduct R A B) C ≃ₐc[R] TensorProduct R A (TensorProduct R B C)

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

Equations

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

@[simp]

theorem Bialgebra.TensorProduct.assoc_tmul {R A B C : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] (x : A) (y : B) (z : C) : (Bialgebra.TensorProduct.assoc R A B C) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = x ⊗ₜ[R] y ⊗ₜ[R] z

@[simp]

theorem Bialgebra.TensorProduct.assoc_symm_tmul {R A B C : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] (x : A) (y : B) (z : C) : (Bialgebra.TensorProduct.assoc R A B C).symm (x ⊗ₜ[R] y ⊗ₜ[R] z) = (x ⊗ₜ[R] y) ⊗ₜ[R] z

@[simp]

theorem Bialgebra.TensorProduct.assoc_toCoalgEquiv {R A B C : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] : ↑(Bialgebra.TensorProduct.assoc R A B C) = Coalgebra.TensorProduct.assoc R A B C

@[simp]

theorem Bialgebra.TensorProduct.assoc_toAlgEquiv {R A B C : Type u} [CommRing R] [Ring A] [Ring B] [Ring C] [Bialgebra R A] [Bialgebra R B] [Bialgebra R C] : ↑(Bialgebra.TensorProduct.assoc R A B C) = Algebra.TensorProduct.assoc R A B C

noncomputable def Bialgebra.TensorProduct.lid (R A : Type u) [CommRing R] [Ring A] [Bialgebra R A] : TensorProduct R R A ≃ₐc[R] A

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

Equations

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

@[simp]

theorem Bialgebra.TensorProduct.lid_toCoalgEquiv {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] : ↑(Bialgebra.TensorProduct.lid R A) = Coalgebra.TensorProduct.lid R A

@[simp]

theorem Bialgebra.TensorProduct.lid_toAlgEquiv {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] : ↑(Bialgebra.TensorProduct.lid R A) = Algebra.TensorProduct.lid R A

@[simp]

theorem Bialgebra.TensorProduct.lid_tmul {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] (r : R) (a : A) : (Bialgebra.TensorProduct.lid R A) (r ⊗ₜ[R] a) = r • a

@[simp]

theorem Bialgebra.TensorProduct.lid_symm_apply {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] (a : A) : (Bialgebra.TensorProduct.lid R A).symm a = 1 ⊗ₜ[R] a

theorem Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] (x : TensorProduct R A R) : (Coalgebra.TensorProduct.rid R A) x = (Algebra.TensorProduct.rid R R A) x

noncomputable def Bialgebra.TensorProduct.rid (R A : Type u) [CommRing R] [Ring A] [Bialgebra R A] : TensorProduct R A R ≃ₐc[R] A

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

Equations

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

@[simp]

theorem Bialgebra.TensorProduct.rid_toCoalgEquiv {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] : ↑(Bialgebra.TensorProduct.rid R A) = Coalgebra.TensorProduct.rid R A

@[simp]

theorem Bialgebra.TensorProduct.rid_toAlgEquiv {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] : ↑(Bialgebra.TensorProduct.rid R A) = Algebra.TensorProduct.rid R R A

@[simp]

theorem Bialgebra.TensorProduct.rid_tmul {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] (r : R) (a : A) : (Bialgebra.TensorProduct.rid R A) (a ⊗ₜ[R] r) = r • a

@[simp]

theorem Bialgebra.TensorProduct.rid_symm_apply {R A : Type u} [CommRing R] [Ring A] [Bialgebra R A] (a : A) : (Bialgebra.TensorProduct.rid R A).symm a = a ⊗ₜ[R] 1

@[reducible, inline]

noncomputable abbrev BialgHom.lTensor {R : Type u} (A : Type u) {B C : Type u} [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} (A : Type u) {B C : Type u} [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)