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

Note that in the case C = A this convolution product conflicts with the (unfortunately global!) group instance on Module.End R A with multiplication defined as composition. As a result, the convolution product is scoped to ConvolutionProduct.

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convMul = { mul := fun (f g : C →ₗ[R] A) => LinearMap.mul' R A ∘ₗ TensorProduct.map f g ∘ₗ CoalgebraStruct.comul }

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 : C →ₗ[R] A) : f * g = mul' R A ∘ₗ TensorProduct.map f g ∘ₗ 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 : C →ₗ[R] A) (c : C) : (f * g) c = (mul' R A) ((TensorProduct.map f g) (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 : C →ₗ[R] A) : (f * g) a = ∑ i ∈ 𝓡.index, f (𝓡.left i) * g (𝓡.right i)

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convNonUnitalNonAssocSemiring = { toAddCommMonoid := LinearMap.addCommMonoid, toMul := LinearMap.convMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

@[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) : toSpanSingleton R A x * toSpanSingleton R A y = 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 : C →ₗ[R] A} {g k : B →ₗ[R] D} : map f g * map h k = map (f * h) (g * k)

@[reducible, inline]

noncomputable abbrev 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 (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.

Equations

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

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 : C →ₗ[R] A) : ↑h ∘ₗ (f * g) = ↑h ∘ₗ f * ↑h ∘ₗ g

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 : C →ₗ[R] A) (h : B →ₗc[R] C) : (f * g) ∘ₗ h.toLinearMap = f ∘ₗ h.toLinearMap * g ∘ₗ h.toLinearMap

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convNonUnitalSemiring = { toNonUnitalNonAssocSemiring := LinearMap.convNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convNonUnitalRing = { toNonUnitalNonAssocRing := LinearMap.convNonUnitalNonAssocRing, mul_assoc := ⋯ }

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 : C →ₗ[R] A) : h.toLinearMap ∘ₗ (f * g) = h.toLinearMap ∘ₗ f * h.toLinearMap ∘ₗ g

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convOne = { one := Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit }

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 = 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) : 1 c = (algebraMap R A) (CoalgebraStruct.counit c)

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

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

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convCommSemiring = { toSemiring := LinearMap.convSemiring, mul_comm := ⋯ }

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

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

@[reducible, inline]

noncomputable abbrev 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 (C →ₗ[R] A)

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

Equations

• LinearMap.convCommRing = { toRing := LinearMap.convRing, mul_comm := ⋯ }