Convolution product on linear maps from a coalgebra to an algebra

This file constructs the ring and algebra 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).

@[instance_reducible]

noncomputable instance LinearMap.convMul {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

theorem LinearMap.convMul_def {R : Type u_1} {A : Type u_3} {C : Type u_5} [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_3} {C : Type u_5} [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_3} {C : Type u_5} {ι : Type u_6} [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)

@[instance_reducible]

noncomputable instance LinearMap.convNonUnitalNonAssocSemiring {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

instance LinearMap.instIsScalarTowerWithConvId {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [Monoid S] [DistribMulAction S A] [SMulCommClass R S A] [IsScalarTower S A A] : IsScalarTower S (WithConv (C →ₗ[R] A)) (WithConv (C →ₗ[R] A))

instance LinearMap.instSMulCommClassWithConvId {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [Monoid S] [DistribMulAction S A] [SMulCommClass R S A] [SMulCommClass S A A] : SMulCommClass S (WithConv (C →ₗ[R] A)) (WithConv (C →ₗ[R] A))

@[simp]

theorem LinearMap.toSpanSingleton_convMul_toSpanSingleton {R : Type u_1} {A : Type u_3} [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_3} {B : Type u_4} {C : Type u_5} [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_7} [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)

@[instance_reducible]

noncomputable instance LinearMap.convNonUnitalNonAssocRing {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

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_3} {B : Type u_4} {C : Type u_5} [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_3} {B : Type u_4} {C : Type u_5} [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

@[instance_reducible]

noncomputable instance LinearMap.convNonUnitalSemiring {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

@[instance_reducible]

noncomputable instance LinearMap.convNonUnitalRing {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

@[instance_reducible]

noncomputable instance LinearMap.instOneWithConvId {R : Type u_1} {A : Type u_3} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] : One (WithConv (C →ₗ[R] A))

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

Equations

• LinearMap.instOneWithConvId = { one := WithConv.toConv (Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) }

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

@[simp]

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

@[simp]

theorem LinearMap.convOne_comp_coalgHom {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] (h : B →ₗc[R] C) : WithConv.ofConv 1 ∘ₗ ↑h = WithConv.ofConv 1

theorem LinearMap.algHom_comp_convMul_distrib {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [Semiring B] [Algebra R B] (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

@[simp]

theorem LinearMap.algHom_comp_convOne {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [Semiring B] [Algebra R B] (h : A →ₐ[R] B) : h.toLinearMap ∘ₗ WithConv.ofConv 1 = WithConv.ofConv 1

@[instance_reducible]

noncomputable instance LinearMap.convSemiring {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

@[instance_reducible]

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

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

Equations

• LinearMap.convAlgebra = Algebra.ofModule ⋯ ⋯

@[simp]

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

@[instance_reducible]

noncomputable instance LinearMap.convCommSemiring {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

@[instance_reducible]

noncomputable instance LinearMap.convRing {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

@[instance_reducible]

noncomputable instance LinearMap.convCommRing {R : Type u_1} {A : Type u_3} {C : Type u_5} [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.

Equations

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

noncomputable def AlgHom.convPostcomp {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Semiring B] [Algebra R B] (h : A →ₐ[R] B) : WithConv (C →ₗ[R] A) →ₐ[R] WithConv (C →ₗ[R] B)

Post-composition by an algebra homomorphism, as a homomorphism of convolution algebras.

Equations

• h.convPostcomp = { toFun := fun (f : WithConv (C →ₗ[R] A)) => WithConv.toConv (h.toLinearMap ∘ₗ f.ofConv), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.convPostcomp_apply_ofConv {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Semiring B] [Algebra R B] (h : A →ₐ[R] B) (f : WithConv (C →ₗ[R] A)) : (h.convPostcomp f).ofConv = h.toLinearMap ∘ₗ f.ofConv

theorem AlgHom.convPostcomp_injective {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Semiring B] [Algebra R B] {h : A →ₐ[R] B} (hh : Function.Injective ⇑h) : Function.Injective ⇑h.convPostcomp

@[simp]

theorem AlgHom.convPostcomp_id {R : Type u_1} {A : Type u_3} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : (AlgHom.id R A).convPostcomp = AlgHom.id R (WithConv (C →ₗ[R] A))

theorem AlgHom.convPostcomp_comp {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Semiring B] [Algebra R B] {D : Type u_7} [Semiring D] [Algebra R D] (h₁ : B →ₐ[R] D) (h₂ : A →ₐ[R] B) : (h₁.comp h₂).convPostcomp = h₁.convPostcomp.comp h₂.convPostcomp

noncomputable def CoalgHom.convPrecomp {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [Coalgebra R B] (h : B →ₗc[R] C) : WithConv (C →ₗ[R] A) →ₐ[R] WithConv (B →ₗ[R] A)

Pre-composition by a coalgebra homomorphism, as a homomorphism of convolution algebras.

Equations

• h.convPrecomp = { toFun := fun (f : WithConv (C →ₗ[R] A)) => WithConv.toConv (f.ofConv ∘ₗ ↑h), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem CoalgHom.convPrecomp_apply_ofConv {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [Coalgebra R B] (h : B →ₗc[R] C) (f : WithConv (C →ₗ[R] A)) : (h.convPrecomp f).ofConv = f.ofConv ∘ₗ ↑h

theorem CoalgHom.convPrecomp_injective {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [Coalgebra R B] {h : B →ₗc[R] C} (hh : Function.Surjective ⇑h) : Function.Injective ⇑h.convPrecomp

@[simp]

theorem CoalgHom.convPrecomp_id {R : Type u_1} {A : Type u_3} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] : (CoalgHom.id R C).convPrecomp = AlgHom.id R (WithConv (C →ₗ[R] A))

theorem CoalgHom.convPrecomp_comp {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [Coalgebra R B] {D : Type u_7} [AddCommMonoid D] [Module R D] [Coalgebra R D] (h₁ : B →ₗc[R] C) (h₂ : D →ₗc[R] B) : (h₁.comp h₂).convPrecomp = h₂.convPrecomp.comp h₁.convPrecomp

theorem CoalgHom.convPrecomp_comp_convPostcomp {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid B] [Module R B] [Coalgebra R B] {D : Type u_7} [Semiring D] [Algebra R D] (h : B →ₗc[R] C) (φ : A →ₐ[R] D) : h.convPrecomp.comp φ.convPostcomp = φ.convPostcomp.comp h.convPrecomp