Comultiplication as a convolution product

Let C be an R-algebra carrying a comultiplication. This file records that, in the convolution monoid of linear maps C →ₗ[R] C ⊗[R] C, comultiplication is the convolution product of the two canonical inclusions c ↦ c ⊗ₜ 1 and c ↦ 1 ⊗ₜ c of C into its tensor square.

The file also provides the exterior convolution product LinearMap.mulTensor: linear maps out of modules M and N, valued in an algebra, applied legwise on M ⊗[R] N and multiplied in the codomain. Its normalization rules (zero, addition, scalars) and its multiplicativity for the convolution product make it the engine for composition-level convolution calculations: convolution products interleave legwise, and composing with a multiplication lands in the image of mulTensor for maps with a suitable multiplicativity law. This file proves that for an algebra map (AlgHom.toConv_toLinearMap_comp_mul'); the Leibniz-rule counterpart for counit-valued derivations is in TauCeti/Algebra/AlgebraicGroup/Tangent/Basic.lean.

Finally, the file records how convolution algebras change with their coefficients. An algebra map g : B →ₐ[R] B' induces an algebra map of convolution algebras by post-composition, and when B' is a B-algebra with a basis over B, taking coordinates identifies the convolution algebra with coefficients in B' with a free module over the one with coefficients in B.

Main declarations

• TauCeti.Coalgebra.comul_eq_convMul_includeLeft_includeRight: comultiplication as the convolution product of the two tensor inclusions.
• TauCeti.Bialgebra.comulPoint_eq_include_mul: the corresponding identity for the algebra-hom points of a commutative bialgebra.
• TauCeti.Bialgebra.toConv_comp_comulAlgHom: the functorial form of the previous identity, after post-composing with an arbitrary algebra map out of the tensor square.
• TauCeti.LinearMap.mulTensor: the exterior convolution product, with its normalization rules and TauCeti.LinearMap.mulTensor_convMul.
• TauCeti.AlgHom.toConv_toLinearMap_comp_mul': an algebra map composed with multiplication is its own exterior square.
• AlgHom.convCompLeft: post-composition with an algebra map, as an algebra map of convolution algebras.
• Module.Basis.convCoordEquiv: the coordinates of a convolution-algebra element in a basis of the coefficients, with Module.Basis.convCoordEquiv_convCompLeft_mul recording that they are linear over the convolution algebra of the smaller coefficient ring.

theorem TauCeti.Coalgebra.comul_eq_convMul_includeLeft_includeRight {R : Type u_1} {C : Type u_2} [CommSemiring R] [Semiring C] [Algebra R C] [CoalgebraStruct R C] : WithConv.toConv CoalgebraStruct.comul = WithConv.toConv Algebra.TensorProduct.includeLeft.toLinearMap * WithConv.toConv Algebra.TensorProduct.includeRight.toLinearMap

Comultiplication is the convolution product of the two tensor inclusions. In the convolution monoid of maps C →ₗ[R] C ⊗[R] C, the product of includeLeft and includeRight multiplies the two legs of Δ c back together in order, which is Δ itself.

Only the comultiplication data is used, so this needs CoalgebraStruct rather than Coalgebra: no coalgebra law, bialgebra compatibility or antipode axiom enters.

theorem TauCeti.Bialgebra.toConv_comp_comulAlgHom {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] {A : Type u_3} [CommSemiring A] [Algebra R A] (phi : TensorProduct R H H →ₐ[R] A) : WithConv.toConv (phi.comp (Bialgebra.comulAlgHom R H)) = WithConv.toConv (phi.comp ↑TensorProduct.includeLeft) * WithConv.toConv (phi.comp ↑TensorProduct.includeRight)

Post-composition splits the comultiplication point into its two inclusions. For any algebra map φ out of the tensor square, the point φ ∘ Δ is the convolution product of φ restricted along the two inclusions.

The convolution monoid here is the one on points of H with values in the commutative algebra A, so H itself need only be a semiring: the tensor square H ⊗[R] H is used solely as the source of φ, never as a convolution target. That is why this is proved from the linear-map identity TauCeti.Coalgebra.comul_eq_convMul_includeLeft_includeRight rather than from TauCeti.Bialgebra.comulPoint_eq_include_mul, which needs H ⊗[R] H to be commutative.

theorem TauCeti.Bialgebra.comulPoint_eq_include_mul {R : Type u_1} [CommSemiring R] {H : Type u_2} [CommSemiring H] [Bialgebra R H] : WithConv.toConv (Bialgebra.comulAlgHom R H) = WithConv.toConv ↑TensorProduct.includeLeft * WithConv.toConv ↑TensorProduct.includeRight

The comultiplication point of a commutative bialgebra is the convolution product of the two canonical tensor-factor points. This is the algebra-hom form of Coalgebra.comul_eq_convMul_includeLeft_includeRight.

def TauCeti.LinearMap.mulTensor {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (s : WithConv (M →ₗ[R] S)) (t : WithConv (N →ₗ[R] S)) : WithConv (TensorProduct R M N →ₗ[R] S)

The exterior convolution product on M ⊗[R] N: apply one factor on each tensor leg and multiply the results in the coefficients. It underlies the Leibniz-rule manipulations for counit-valued derivations: composing with the multiplication of the bialgebra lands in this product's image (there at N = M).

Equations

• TauCeti.LinearMap.mulTensor s t = WithConv.toConv (LinearMap.mul' R S ∘ₗ TensorProduct.map s.ofConv t.ofConv)

@[simp]

theorem TauCeti.LinearMap.mulTensor_apply_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (s : WithConv (M →ₗ[R] S)) (t : WithConv (N →ₗ[R] S)) (x : M) (y : N) : (mulTensor s t).ofConv (x ⊗ₜ[R] y) = s.ofConv x * t.ofConv y

The exterior product evaluates a pure tensor legwise and multiplies the results in the coefficients.

@[simp]

theorem TauCeti.LinearMap.mulTensor_zero_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (t : WithConv (N →ₗ[R] S)) : mulTensor 0 t = 0

The exterior product vanishes when the left factor is zero.

@[simp]

theorem TauCeti.LinearMap.mulTensor_zero_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (s : WithConv (M →ₗ[R] S)) : mulTensor s 0 = 0

The exterior product vanishes when the right factor is zero.

@[simp]

theorem TauCeti.LinearMap.mulTensor_add_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (s₁ s₂ : WithConv (M →ₗ[R] S)) (t : WithConv (N →ₗ[R] S)) : mulTensor (s₁ + s₂) t = mulTensor s₁ t + mulTensor s₂ t

The exterior product is additive in the left factor.

@[simp]

theorem TauCeti.LinearMap.mulTensor_add_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (s : WithConv (M →ₗ[R] S)) (t₁ t₂ : WithConv (N →ₗ[R] S)) : mulTensor s (t₁ + t₂) = mulTensor s t₁ + mulTensor s t₂

The exterior product is additive in the right factor.

@[simp]

theorem TauCeti.LinearMap.mulTensor_smul_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (r : R) (s : WithConv (M →ₗ[R] S)) (t : WithConv (N →ₗ[R] S)) : mulTensor (r • s) t = r • mulTensor s t

Scalars pull out of the left factor of the exterior product.

@[simp]

theorem TauCeti.LinearMap.mulTensor_smul_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] (r : R) (s : WithConv (M →ₗ[R] S)) (t : WithConv (N →ₗ[R] S)) : mulTensor s (r • t) = r • mulTensor s t

Scalars pull out of the right factor of the exterior product.

@[simp]

theorem TauCeti.AlgHom.toConv_toLinearMap_comp_mul' {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {A : Type u_5} [Semiring A] [Algebra R A] (g : A →ₐ[R] S) : WithConv.toConv (g.toLinearMap ∘ₗ LinearMap.mul' R A) = LinearMap.mulTensor (WithConv.toConv g.toLinearMap) (WithConv.toConv g.toLinearMap)

An algebra-map point composed with multiplication is its own exterior square: the multiplicativity of the point, in convolution form.

@[simp]

theorem TauCeti.LinearMap.mulTensor_convMul {R : Type u_1} {C : Type u_2} {D : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] [AddCommMonoid D] [Module R D] [CoalgebraStruct R D] [CommSemiring S] [Algebra R S] (s u : WithConv (C →ₗ[R] S)) (t v : WithConv (D →ₗ[R] S)) : mulTensor s t * mulTensor u v = mulTensor (s * u) (t * v)

The exterior product is multiplicative for convolution: products interleave legwise. Only the comultiplication data on each leg is used — no multiplication on the sources and no bialgebra compatibility — so the two legs may be distinct coalgebras.

noncomputable def AlgHom.convCompLeft {R : Type u_1} {B : Type u_2} {B' : Type u_3} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring B'] [Algebra R B'] (g : B →ₐ[R] B') (C : Type u_4) [AddCommMonoid C] [Module R C] [Coalgebra R C] : WithConv (C →ₗ[R] B) →ₐ[R] WithConv (C →ₗ[R] B')

Post-composition with an algebra homomorphism g : B →ₐ[R] B' of coefficient algebras, as an algebra homomorphism between the convolution algebras of linear maps out of a coalgebra C.

Equations

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

@[simp]

theorem AlgHom.convCompLeft_apply {R : Type u_1} {B : Type u_2} {B' : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring B] [Algebra R B] [Semiring B'] [Algebra R B'] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : B →ₐ[R] B') (f : WithConv (C →ₗ[R] B)) : (g.convCompLeft C) f = WithConv.toConv (g.toLinearMap ∘ₗ f.ofConv)

g.convCompLeft C post-composes with g.

noncomputable def Module.Basis.convCoordEquiv {ι : Type u_1} {B : Type u_2} {B' : Type u_3} [Finite ι] [Semiring B] [AddCommMonoid B'] [Module B B'] (b : Basis ι B B') (R : Type u_4) [CommSemiring R] [Algebra R B] [Module R B'] [IsScalarTower R B B'] (C : Type u_5) [AddCommMonoid C] [Module R C] : WithConv (C →ₗ[R] B') ≃ₗ[R] ι → WithConv (C →ₗ[R] B)

A basis of B' over B identifies linear maps C → B' with families of linear maps C → B, by taking coordinates.

Equations

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

@[simp]

theorem Module.Basis.convCoordEquiv_apply {ι : Type u_1} {B : Type u_2} {B' : Type u_3} {R : Type u_4} {C : Type u_5} [Finite ι] [CommSemiring R] [AddCommMonoid C] [Module R C] [Semiring B] [AddCommMonoid B'] [Module B B'] [Algebra R B] [Module R B'] [IsScalarTower R B B'] (b : Basis ι B B') (φ : WithConv (C →ₗ[R] B')) (i : ι) : (b.convCoordEquiv R C) φ i = WithConv.toConv (↑R (b.coord i) ∘ₗ φ.ofConv)

The i-th component of b.convCoordEquiv R C φ is the i-th coordinate of φ.

@[simp]

theorem Module.Basis.convCoordEquiv_symm_apply {ι : Type u_1} {B : Type u_2} {B' : Type u_3} {R : Type u_4} {C : Type u_5} [Finite ι] [CommSemiring R] [AddCommMonoid C] [Module R C] [Semiring B] [AddCommMonoid B'] [Module B B'] [Algebra R B] [Module R B'] [IsScalarTower R B B'] (b : Basis ι B B') (v : ι → WithConv (C →ₗ[R] B)) : (b.convCoordEquiv R C).symm v = WithConv.toConv (↑R ↑b.equivFun.symm ∘ₗ LinearMap.pi fun (i : ι) => (v i).ofConv)

The inverse of b.convCoordEquiv R C reassembles a family of coordinate maps.

theorem Module.Basis.convCoordEquiv_convCompLeft_mul {ι : Type u_1} {B : Type u_2} {B' : Type u_3} {R : Type u_4} {C : Type u_5} [Finite ι] [CommSemiring R] [AddCommMonoid C] [Module R C] [CommSemiring B] [Semiring B'] [Algebra B B'] [Algebra R B] [Algebra R B'] [IsScalarTower R B B'] [Coalgebra R C] (b : Basis ι B B') (f : WithConv (C →ₗ[R] B)) (φ : WithConv (C →ₗ[R] B')) (i : ι) : (b.convCoordEquiv R C) (((IsScalarTower.toAlgHom R B B').convCompLeft C) f * φ) i = f * (b.convCoordEquiv R C) φ i

Taking coordinates in a basis of B' over B is linear over the convolution algebra with coefficients in B, which acts on maps into B' through post-composition with algebraMap B B'.