Documentation

TauCeti.Algebra.Coalgebra.Comodule.Convolution

The convolution algebra acts on a comodule #

Contracting a right coaction against a linear functional gives an endomorphism of the comodule. Coassociativity makes this an algebra homomorphism from the convolution algebra of the coalgebra's dual. Comodule morphisms intertwine these actions. Restricting this homomorphism to counit-valued derivations gives the differentiated action of an affine group.

References #

source
@[simp]
theorem TauCeti.Comodule.coactComponent_counit {R : Type u_1} {C : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] :
coactComponent CoalgebraStruct.counit = LinearMap.id

Contracting a coaction against the counit is the identity.

source
noncomputable def TauCeti.Comodule.convolutionAction {R : Type u_1} {C : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] :
WithConv (C →ₗ[R] R) →ₐ[R] Module.End R M

The convolution algebra on the linear dual of the coalgebra acts by contraction of the coaction.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.convolutionAction_apply {R : Type u_1} {C : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (f : WithConv (C →ₗ[R] R)) (m : M) :
    (convolutionAction f) m = f.ofConv.tensorComponent (coact m)

    Evaluating the convolution action contracts the coaction against the underlying functional.

    source
    @[simp]
    theorem TauCeti.Comodule.Hom.map_convolutionAction {R : Type u_1} {C : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (g : WithConv (C →ₗ[R] R)) (m : M) :
    f ((convolutionAction g) m) = (convolutionAction g) (f m)

    Comodule morphisms intertwine the convolution actions.