Convolution product on bialgebra homs

This file constructs the ring structure on algebra homs C → A where C is a bialgebra and A an algebra, and also the ring structure on bialgebra homs C → A where C and A are bialgebras. Both multiplications are given by

         |
         μ
|   |   / \
f * g = f g
|   |   \ /
         δ
         |

diagrammatically, where μ stands for multiplication and δ for comultiplication.

@[instance_reducible]

noncomputable instance AlgHom.instOneWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : One (WithConv (C →ₐ[R] A))

Equations

• AlgHom.instOneWithConv = { one := WithConv.toConv ((Algebra.ofId R A).comp (Bialgebra.counitAlgHom R C)) }

@[instance_reducible]

noncomputable instance AlgHom.instMulWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : Mul (WithConv (C →ₐ[R] A))

Equations

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

@[instance_reducible]

noncomputable instance AlgHom.instPowWithConvNat {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : Pow (WithConv (C →ₐ[R] A)) ℕ

Equations

• AlgHom.instPowWithConvNat = { pow := fun (f : WithConv (C →ₐ[R] A)) (n : ℕ) => npowRec n f }

theorem AlgHom.convOne_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : 1 = WithConv.toConv ((Algebra.ofId R A).comp (Bialgebra.counitAlgHom R C))

theorem AlgHom.convMul_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f g : WithConv (C →ₐ[R] A)) : f * g = WithConv.toConv ((Algebra.TensorProduct.lmul' R).comp ((Algebra.TensorProduct.map f.ofConv g.ofConv).comp (Bialgebra.comulAlgHom R C)))

@[simp]

theorem AlgHom.convOne_apply {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (c : C) : (WithConv.ofConv 1) c = (algebraMap R A) (CoalgebraStruct.counit c)

theorem AlgHom.convMul_apply {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f g : WithConv (C →ₐ[R] A)) (c : C) : (f * g).ofConv c = (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (CoalgebraStruct.comul c)

@[simp]

theorem AlgHom.toLinearMap_convOne {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : WithConv.toConv (WithConv.ofConv 1).toLinearMap = 1

@[simp]

theorem AlgHom.toLinearMap_convMul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f g : WithConv (C →ₐ[R] A)) : WithConv.toConv (f * g).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap * WithConv.toConv g.ofConv.toLinearMap

@[simp]

theorem AlgHom.toLinearMap_convPow {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f : WithConv (C →ₐ[R] A)) (n : ℕ) : WithConv.toConv (f ^ n).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap ^ n

theorem AlgHom.convMul_comp_bialgHom_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Semiring C] [Bialgebra R C] [Algebra R A] [Bialgebra R B] (f g : WithConv (C →ₐ[R] A)) (h : B →ₐc[R] C) : (f * g).ofConv.comp ↑h = (WithConv.toConv (f.ofConv.comp ↑h) * WithConv.toConv (g.ofConv.comp ↑h)).ofConv

theorem AlgHom.comp_convMul_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Semiring C] [Bialgebra R C] [Algebra R A] [Algebra R B] (h : A →ₐ[R] B) (f g : WithConv (C →ₐ[R] A)) : h.comp (f * g).ofConv = (WithConv.toConv (h.comp f.ofConv) * WithConv.toConv (h.comp g.ofConv)).ofConv

@[instance_reducible]

noncomputable instance AlgHom.instMonoidWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] : Monoid (WithConv (C →ₐ[R] A))

Equations

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

@[instance_reducible]

noncomputable instance AlgHom.instCommMonoidWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] [Coalgebra.IsCocomm R C] : CommMonoid (WithConv (C →ₐ[R] A))

Equations

• AlgHom.instCommMonoidWithConv = { toMonoid := AlgHom.instMonoidWithConv, mul_comm := ⋯ }

theorem BialgHom.convPrecomp_eq_convPostcomp {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] [Semiring C] [Algebra R C] [Coalgebra R C] (f : A →ₐc[R] C) {g : C →ₗ[R] C} {g' : A →ₗ[R] A} (h : Function.Semiconj ⇑f ⇑g' ⇑g) : f.convPrecomp (WithConv.toConv g) = (↑f).convPostcomp (WithConv.toConv g')

@[instance_reducible]

noncomputable instance BialgHom.instOneWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] : One (WithConv (C →ₐc[R] A))

Equations

• BialgHom.instOneWithConv = { one := WithConv.toConv ((Bialgebra.unitBialgHom R A).comp (Bialgebra.counitBialgHom R C)) }

theorem BialgHom.convOne_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] : 1 = WithConv.toConv ((Bialgebra.unitBialgHom R A).comp (Bialgebra.counitBialgHom R C))

@[simp]

theorem BialgHom.convOne_apply {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] (c : C) : (WithConv.ofConv 1) c = (algebraMap R A) (CoalgebraStruct.counit c)

@[simp]

theorem BialgHom.toLinearMap_convOne {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] : WithConv.toConv ↑(WithConv.ofConv 1) = 1

@[simp]

theorem BialgHom.toAlgHom_convOne {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] : WithConv.toConv ↑(WithConv.ofConv 1) = 1

@[instance_reducible]

noncomputable instance BialgHom.instMulWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] : Mul (WithConv (C →ₐc[R] A))

Equations

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

@[instance_reducible]

noncomputable instance BialgHom.instPowWithConvNat {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] : Pow (WithConv (C →ₐc[R] A)) ℕ

Equations

• BialgHom.instPowWithConvNat = { pow := fun (f : WithConv (C →ₐc[R] A)) (n : ℕ) => npowRec n f }

theorem BialgHom.convMul_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)) : f * g = WithConv.toConv ((Bialgebra.mulBialgHom R A).comp ((Bialgebra.TensorProduct.map f.ofConv g.ofConv).comp (Bialgebra.comulBialgHom R C)))

theorem BialgHom.toLinearMap_convMul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)) : WithConv.toConv (f * g).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap * WithConv.toConv g.ofConv.toLinearMap

@[simp]

theorem BialgHom.toAlgHom_convMul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)) : WithConv.toConv ↑(f * g).ofConv = WithConv.toConv ↑f.ofConv * WithConv.toConv ↑g.ofConv

theorem BialgHom.toLinearMap_convPow {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f : WithConv (C →ₐc[R] A)) (n : ℕ) : WithConv.toConv (f ^ n).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap ^ n

@[simp]

theorem BialgHom.toAlgHom_convPow {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f : WithConv (C →ₐc[R] A)) (n : ℕ) : WithConv.toConv ↑(f ^ n).ofConv = WithConv.toConv ↑f.ofConv ^ n

@[instance_reducible]

noncomputable instance BialgHom.instCommMonoidWithConv {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] : CommMonoid (WithConv (C →ₐc[R] A))

Equations

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