Convolution product on linear maps from a coalgebra to an algebra

This file constructs the ring structure on linear maps C → A where C is a coalgebra and A an algebra, where multiplication is given by (f * g)(x) = ∑ f x₍₁₎ * g x₍₂₎ in Sweedler notation or

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

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

Implementation notes

Because there is a global multiplication instance on Module.End R A (defined as composition), which is mathematically distinct from this product, we provide this instance on WithConv (C →ₗ[R] A).

noncomputable instance LinearMap.convMul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] : Mul (WithConv (C →ₗ[R] A))

Convolution product on linear maps from a coalgebra to an algebra.

theorem LinearMap.convMul_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (f g : WithConv (C →ₗ[R] A)) : f * g = WithConv.toConv (mul' R A ∘ₗ TensorProduct.map f.ofConv g.ofConv ∘ₗ CoalgebraStruct.comul)

@[simp]

theorem LinearMap.convMul_apply {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (f g : WithConv (C →ₗ[R] A)) (c : C) : (f * g).ofConv c = (mul' R A) ((TensorProduct.map f.ofConv g.ofConv) (CoalgebraStruct.comul c))

theorem Coalgebra.Repr.convMul_apply {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] {a : C} (𝓡 : Repr R a) (f g : WithConv (C →ₗ[R] A)) : (f * g).ofConv a = ∑ i ∈ 𝓡.index, f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i)

noncomputable instance LinearMap.convNonUnitalNonAssocSemiring {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] : NonUnitalNonAssocSemiring (WithConv (C →ₗ[R] A))

Non-unital and non-associative convolution semiring structure on linear maps from a coalgebra to a non-unital non-associative algebra.

@[simp]

theorem LinearMap.toSpanSingleton_convMul_toSpanSingleton {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (x y : A) : WithConv.toConv (toSpanSingleton R A x) * WithConv.toConv (toSpanSingleton R A y) = WithConv.toConv (toSpanSingleton R A (x * y))

theorem TensorProduct.map_convMul_map {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] {D : Type u_5} [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] [NonUnitalNonAssocSemiring D] [Module R D] [SMulCommClass R D D] [IsScalarTower R D D] {f h : WithConv (C →ₗ[R] A)} {g k : WithConv (B →ₗ[R] D)} : WithConv.toConv (map f.ofConv g.ofConv) * WithConv.toConv (map h.ofConv k.ofConv) = WithConv.toConv (map (f * h).ofConv (g * k).ofConv)

noncomputable instance LinearMap.convNonUnitalNonAssocRing {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] : NonUnitalNonAssocRing (WithConv (C →ₗ[R] A))

Non-unital and non-associative convolution ring structure on linear maps from a coalgebra to a non-unital and non-associative algebra.

theorem LinearMap.nonUnitalAlgHom_comp_convMul_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (h : A →ₙₐ[R] B) (f g : WithConv (C →ₗ[R] A)) : ↑h ∘ₗ (f * g).ofConv = (WithConv.toConv (↑h ∘ₗ f.ofConv) * WithConv.toConv (↑h ∘ₗ g.ofConv)).ofConv

theorem LinearMap.convMul_comp_coalgHom_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] (f g : WithConv (C →ₗ[R] A)) (h : B →ₗc[R] C) : (f * g).ofConv ∘ₗ h.toLinearMap = (WithConv.toConv (f.ofConv ∘ₗ h.toLinearMap) * WithConv.toConv (g.ofConv ∘ₗ h.toLinearMap)).ofConv

noncomputable instance LinearMap.convNonUnitalSemiring {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : NonUnitalSemiring (WithConv (C →ₗ[R] A))

Non-unital convolution semiring structure on linear maps from a coalgebra to a non-unital algebra.

noncomputable instance LinearMap.convNonUnitalRing {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalRing A] [AddCommMonoid C] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Module R C] [Coalgebra R C] : NonUnitalRing (WithConv (C →ₗ[R] A))

Non-unital convolution ring structure on linear maps from a coalgebra to a non-unital algebra.

theorem LinearMap.algHom_comp_convMul_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (h : A →ₐ[R] B) (f g : WithConv (C →ₗ[R] A)) : h.toLinearMap ∘ₗ (f * g).ofConv = (WithConv.toConv (h.toLinearMap ∘ₗ f.ofConv) * WithConv.toConv (h.toLinearMap ∘ₗ g.ofConv)).ofConv

noncomputable instance LinearMap.convOne {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : One (WithConv (C →ₗ[R] A))

Convolution unit on linear maps from a coalgebra to an algebra.

theorem LinearMap.convOne_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : 1 = WithConv.toConv (Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit)

@[simp]

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

noncomputable instance LinearMap.convSemiring {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Semiring (WithConv (C →ₗ[R] A))

Convolution semiring structure on linear maps from a coalgebra to an algebra.

noncomputable instance LinearMap.convCommSemiring {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid C] [Algebra R A] [Module R C] [Coalgebra R C] [Coalgebra.IsCocomm R C] : CommSemiring (WithConv (C →ₗ[R] A))

Commutative convolution semiring structure on linear maps from a cocommutative coalgebra to an algebra.

noncomputable instance LinearMap.convRing {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [Ring A] [AddCommMonoid C] [Algebra R A] [Module R C] [Coalgebra R C] : Ring (WithConv (C →ₗ[R] A))

Convolution ring structure on linear maps from a coalgebra to an algebra.

noncomputable instance LinearMap.convCommRing {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommRing A] [AddCommMonoid C] [Algebra R A] [Module R C] [Coalgebra R C] [Coalgebra.IsCocomm R C] : CommRing (WithConv (C →ₗ[R] A))

Commutative convolution ring structure on linear maps from a cocommutative coalgebra to an algebra.