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.

source

@[implicit_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)) }

source

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

source

@[implicit_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 }

source

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))

source

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)))

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

@[implicit_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 := ⋯ }

source

@[implicit_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)) }

source

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))

source

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

source

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

source

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

source

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

source

@[implicit_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 }

source

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)))

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.RingTheory.Bialgebra.Convolution

Convolution product on bialgebra homs #