@[simp]

theorem Bialgebra.counitAlgHom_comp_includeRight {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Bialgebra R B] : (AlgHom.restrictScalars R (counitAlgHom A (TensorProduct R A B))).comp Algebra.TensorProduct.includeRight = (Algebra.ofId R A).comp (counitAlgHom R B)

theorem Bialgebra.comul_includeRight {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Bialgebra R B] [Algebra R A] : (↑(comulAlgHom A (TensorProduct R A B))).comp ↑Algebra.TensorProduct.includeRight = (Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp ↑(comulAlgHom R B)

noncomputable 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 = { toAddHom := (LinearMap.mul' R A).toAddHom, map_smul' := ⋯, counit_comp := ⋯, map_comp_comul := ⋯ }

@[simp]

theorem Bialgebra.mulCoalgHom_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (a b : A) : (mulCoalgHom R A) (a ⊗ₜ[R] b) = a * b

noncomputable def Bialgebra.TensorProduct.comm (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [CommSemiring 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) ⋯ ⋯

noncomputable 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 = { toFun := (↑↑(Algebra.TensorProduct.lmul' R).toRingHom).toFun, map_add' := ⋯, map_smul' := ⋯, counit_comp := ⋯, map_comp_comul := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Bialgebra.mulBialgHom_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] (a b : A) : (mulBialgHom R A) (a ⊗ₜ[R] b) = a * b

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

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] [CommSemiring A] [Bialgebra R A] [Coalgebra.IsCocomm R A] : (TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A) = comulBialgHom R A

def Coalgebra.Repr.tmul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a b : A} (ℛa : Repr R a) (ℛb : Repr R b) : Repr R (a ⊗ₜ[R] b)

Representations of a and b yield a representation of a ⊗ b.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Coalgebra.Repr.tmul_index {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a b : A} (ℛa : Repr R a) (ℛb : Repr R b) : (ℛa.tmul ℛb).index = ℛa.index ×ˢ ℛb.index

@[simp]

theorem Coalgebra.Repr.tmul_left {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a b : A} (ℛa : Repr R a) (ℛb : Repr R b) (i : ℛa.ι × ℛb.ι) : (ℛa.tmul ℛb).left i = ℛa.left i.1 ⊗ₜ[R] ℛb.left i.2

@[simp]

theorem Coalgebra.Repr.tmul_right {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a b : A} (ℛa : Repr R a) (ℛb : Repr R b) (i : ℛa.ι × ℛb.ι) : (ℛa.tmul ℛb).right i = ℛa.right i.1 ⊗ₜ[R] ℛb.right i.2

@[simp]

theorem Coalgebra.Repr.tmul_ι {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a b : A} (ℛa : Repr R a) (ℛb : Repr R b) : (ℛa.tmul ℛb).ι = (ℛa.ι × ℛb.ι)

noncomputable def Coalgebra.Repr.mul {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) : Repr R (a₁ * a₂)

Representations of a₁ and a₂ yield a representation of a₁ * a₂.

Equations

• ℛ₁.mul ℛ₂ = (ℛ₁.tmul ℛ₂).induced (Bialgebra.mulCoalgHom R A)

@[simp]

theorem Coalgebra.Repr.mul_left {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) (a✝ : (ℛ₁.tmul ℛ₂).ι) : (ℛ₁.mul ℛ₂).left a✝ = ℛ₁.left a✝.1 * ℛ₂.left a✝.2

@[simp]

theorem Coalgebra.Repr.mul_right {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) (a✝ : (ℛ₁.tmul ℛ₂).ι) : (ℛ₁.mul ℛ₂).right a✝ = ℛ₁.right a✝.1 * ℛ₂.right a✝.2

@[simp]

theorem Coalgebra.Repr.mul_ι {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) : (ℛ₁.mul ℛ₂).ι = (ℛ₁.ι × ℛ₂.ι)

@[simp]

theorem Coalgebra.Repr.mul_index_val {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) : (ℛ₁.mul ℛ₂).index.val = ℛ₁.index.val ×ˢ ℛ₂.index.val

@[simp]

theorem Coalgebra.Repr.mul_index {R : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring A] [Bialgebra R A] {a₁ a₂ : A} (ℛ₁ : Repr R a₁) (ℛ₂ : Repr R a₂) : (ℛ₁.mul ℛ₂).index = ℛ₁.index ×ˢ ℛ₂.index