R-algebra structure on the convolution semiring WithConv (C →ₗ[R] A)

Mathlib's Mathlib.RingTheory.Coalgebra.Convolution provides the convolution Semiring / CommSemiring / Ring / CommRing structures on WithConv (C →ₗ[R] A) (for C a coalgebra and A an algebra, with appropriate hypotheses). It does not provide an Algebra R instance, even though one exists naturally: scalars act on linear maps in a way that commutes with convolution (because both the convolution and the scalar action factor through mul' on A, which is R-linear).

This file supplies the missing Algebra R (WithConv (C →ₗ[R] A)) instance via Algebra.ofModule. The two compatibility hypotheses reduce to TensorProduct.map_smul_left / map_smul_right plus the R-linearity of mul' R A and comul.

[UPSTREAM] candidate

Natural home is Mathlib/RingTheory/Coalgebra/Convolution.lean, immediately after convSemiring.

@[implicit_reducible]

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

Convolution R-algebra structure on WithConv (C →ₗ[R] A).

Equations

• LinearMap.convAlgebra = Algebra.ofModule ⋯ ⋯

@[simp]

theorem LinearMap.convAlgebraMap_apply {R : Type u_1} {C : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] (r : R) (c : C) : ((algebraMap R (WithConv (C →ₗ[R] A))) r).ofConv c = r • (algebraMap R A) (CoalgebraStruct.counit c)