The weight decomposition of a comodule over a monoid algebra

Let R[G] be the monoid algebra of a type G over a commutative semiring R. Its coalgebra structure makes every single g 1 a group-like element. This file proves that a right R[G]-comodule V is the internal direct sum of its weight submodules

weightSpace R G V g = {v | ρ v = v ⊗ single g 1},

each of which is a subcomodule. When G is a commutative group, R[G] is the coordinate Hopf algebra of the diagonalizable group D(G), and this says that its representations decompose into character spaces.

The proof is the classical one and uses nothing beyond the comodule axioms. Writing the coaction of v as ρ v = ∑ g, v g ⊗ single g 1, which is possible because R[G] is free on the group-like elements, the counit axiom says that the coefficients sum to v and coassociativity says that the h-coefficient of v g is v g when h = g and 0 otherwise. The coefficient maps are therefore orthogonal idempotents with images the weight submodules, which gives both the spanning and the independence half of the decomposition.

Main definitions

• TauCeti.Comodule.tensorCoeffEquiv: the coefficients of an element of V ⊗[R] R[G], as a finitely supported family.
• TauCeti.Comodule.weightDecomposition: the weight components of a comodule, as a linear map to finitely supported families.
• TauCeti.Comodule.weightProj: the projection onto the g-weight component.
• TauCeti.Comodule.weightSpace: the g-weight submodule, where the coaction is v ↦ v ⊗ g.
• TauCeti.Comodule.weightSubcomodule: the weight submodule as a subcomodule.

Main results

• TauCeti.Comodule.weightDecomposition_sum: the weight components of a vector sum to it.
• TauCeti.Comodule.weightProj_weightProj_self and TauCeti.Comodule.weightProj_weightProj_of_ne: the weight projections are orthogonal idempotents.
• TauCeti.Comodule.weightProj_mem_weightSpace: each weight component lies in its weight submodule.
• TauCeti.Comodule.isInternal_weightSpace: a comodule over a monoid algebra is the internal direct sum of its weight submodules.
• TauCeti.Comodule.endOfPoint_tmul_of_mem_weightSpace: an algebra map out of R[G] acts on the g-weight submodule by multiplication by its value at the group-like element single g 1.
• TauCeti.Comodule.Hom.map_mem_weightSpace: a comodule morphism preserves the weight submodules.
• TauCeti.Comodule.weightProj_mem_subcomodule: every subcomodule is stable under the weight projections.
• TauCeti.Comodule.range_weightProj: the g-weight submodule is the range of the g-weight projection.
• TauCeti.Comodule.finite_setOf_weightSpace_ne_bot: a comodule finitely generated as a module has only finitely many weights.

Implementation notes

Only the coalgebra structure of R[G] is used, so G is an arbitrary type: no multiplication on G and no algebra structure on R[G] enter the argument. That R[G] is free on G is used through TensorProduct.finsuppScalarRight, which presents V ⊗[R] R[G] as the finitely supported functions G →₀ V and so supplies the finite support of the weight decomposition for free; this is also the only place where decidable equality on G is used internally, and it is discharged classically.

References

For a commutative group G, this specializes to the standard statement that representations of a diagonalizable group are diagonalizable; see Waterhouse, Introduction to Affine Group Schemes, §3.2, and Milne, Algebraic Groups (2017), Theorem 12.12.

It supplies a prerequisite for the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap: Layer 6 asks for the linear reductivity of tori ("over an algebraically closed field of characteristic p, a connected group is linearly reductive iff it is a torus"), of which this is the substantive direction for a split torus, and Layer 7's root datum of a split pair (G, T) is read off the weight decomposition of Lie G under T that this file provides. The diagonalizable group D(G) = Spec R[G] itself is in TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Basic.

Coefficients of a tensor with a monoid algebra

noncomputable def TauCeti.Comodule.monoidCoeff (R : Type u) (G : Type v) [CommSemiring R] (g : G) : MonoidAlgebra R G →ₗ[R] R

The coefficient functional at a basis element of a monoid algebra.

Equations

• TauCeti.Comodule.monoidCoeff R G g = Finsupp.lapply g ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv R)

@[simp]

theorem TauCeti.Comodule.monoidCoeff_apply (R : Type u) (G : Type v) [CommSemiring R] (g : G) (x : MonoidAlgebra R G) : (monoidCoeff R G g) x = x.coeff g

noncomputable def TauCeti.Comodule.tensorCoeffEquiv (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] : TensorProduct R V (MonoidAlgebra R G) ≃ₗ[R] G →₀ V

The coefficients of an element of V ⊗[R] R[G], as a finitely supported family.

Equations

• TauCeti.Comodule.tensorCoeffEquiv R G V = (LinearEquiv.lTensor V (MonoidAlgebra.coeffLinearEquiv R)).trans (TensorProduct.finsuppScalarRight R R V G)

@[simp]

theorem TauCeti.Comodule.tensorCoeffEquiv_apply {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] (t : TensorProduct R V (MonoidAlgebra R G)) (g : G) : ((tensorCoeffEquiv R G V) t) g = (monoidCoeff R G g).tensorComponent t

The coefficient family of an element of V ⊗[R] R[G] is given by the coefficient maps.

@[simp]

theorem TauCeti.Comodule.tensorCoeffEquiv_tmul {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] (v : V) (x : MonoidAlgebra R G) : (tensorCoeffEquiv R G V) (v ⊗ₜ[R] x) = Finsupp.mapRange (fun (r : R) => r • v) ⋯ x.coeff

The coefficient family of a pure tensor scales the vector by the coefficients.

@[simp]

theorem TauCeti.Comodule.tensorCoeffEquiv_symm_single {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] (g : G) (v : V) : (tensorCoeffEquiv R G V).symm (Finsupp.single g v) = v ⊗ₜ[R] MonoidAlgebra.single g 1

The weight components of a comodule

noncomputable def TauCeti.Comodule.weightProj (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) : V →ₗ[R] V

The projection of a comodule over R[G] onto its g-weight component.

Equations

• TauCeti.Comodule.weightProj R G V g = TauCeti.Comodule.coactComponent (TauCeti.Comodule.monoidCoeff R G g)

theorem TauCeti.Comodule.weightProj_apply {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) (v : V) : (weightProj R G V g) v = (monoidCoeff R G g).tensorComponent (coact v)

The g-weight component of v is the g-th coefficient of its coaction.

This is deliberately not a simp lemma: weightProj_weightProj_self and weightProj_weightProj_of_ne are the simp-normal form of a composite of weight projections, and they could never fire if simp first unfolded every weightProj to a coefficient of a coaction.

noncomputable def TauCeti.Comodule.weightDecomposition (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] : V →ₗ[R] G →₀ V

The weight components of a comodule over R[G], read off its coaction as a finitely supported family.

Equations

• TauCeti.Comodule.weightDecomposition R G V = ↑(TauCeti.Comodule.tensorCoeffEquiv R G V) ∘ₗ TauCeti.Comodule.coact

@[simp]

theorem TauCeti.Comodule.weightDecomposition_apply {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (v : V) (g : G) : ((weightDecomposition R G V) v) g = (weightProj R G V g) v

theorem TauCeti.Comodule.coact_eq_symm_weightDecomposition {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (v : V) : coact v = (tensorCoeffEquiv R G V).symm ((weightDecomposition R G V) v)

The coaction is determined by the weight components.

The counit axiom: the weight components sum to the vector

theorem TauCeti.Comodule.weightDecomposition_sum {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (v : V) : (((weightDecomposition R G V) v).sum fun (x : G) (w : V) => w) = v

The weight components of a vector sum to it. This is the counit axiom of the coaction.

Coassociativity: the weight projections are orthogonal idempotents

@[simp]

theorem TauCeti.Comodule.weightProj_weightProj_self {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) (v : V) : (weightProj R G V g) ((weightProj R G V g) v) = (weightProj R G V g) v

The weight projections are idempotent.

@[simp]

theorem TauCeti.Comodule.weightProj_weightProj_of_ne {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {h g : G} (hne : h ≠ g) (v : V) : (weightProj R G V h) ((weightProj R G V g) v) = 0

The weight projections at distinct indices are orthogonal.

The weight submodules

def TauCeti.Comodule.weightSpace (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) : Submodule R V

The g-weight submodule of a comodule over R[G]: the vectors whose coaction is v ↦ v ⊗ single g 1.

Equations

• TauCeti.Comodule.weightSpace R G V g = { carrier := {v : V | TauCeti.Comodule.coact v = v ⊗ₜ[R] MonoidAlgebra.single g 1}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.Comodule.mem_weightSpace {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {g : G} {v : V} : v ∈ weightSpace R G V g ↔ coact v = v ⊗ₜ[R] MonoidAlgebra.single g 1

theorem TauCeti.Comodule.weightProj_of_mem {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {g : G} {v : V} (hv : v ∈ weightSpace R G V g) : (weightProj R G V g) v = v

On its own weight submodule the weight projection is the identity.

theorem TauCeti.Comodule.weightProj_of_mem_of_ne {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {h g : G} (hne : h ≠ g) {v : V} (hv : v ∈ weightSpace R G V g) : (weightProj R G V h) v = 0

A weight projection kills the weight submodules at all other indices.

theorem TauCeti.Comodule.weightProj_mem_weightSpace {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) (v : V) : (weightProj R G V g) v ∈ weightSpace R G V g

Each weight component lies in its weight submodule.

@[simp]

theorem TauCeti.Comodule.coact_weightProj {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) (v : V) : coact ((weightProj R G V g) v) = (weightProj R G V g) v ⊗ₜ[R] MonoidAlgebra.single g 1

The coaction on a weight component is diagonal. This is weightProj_mem_weightSpace in the simp normal form of membership in weightSpace, and is what discharges such membership goals.

theorem TauCeti.Comodule.iSup_weightSpace_eq_top (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] : ⨆ (g : G), weightSpace R G V g = ⊤

The weight submodules span the whole comodule.

theorem TauCeti.Comodule.iSupIndep_weightSpace (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] : iSupIndep (weightSpace R G V)

The weight submodules are independent.

theorem TauCeti.Comodule.isInternal_weightSpace (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] : DirectSum.IsInternal (weightSpace R G V)

A comodule over a monoid algebra is the internal direct sum of its weight submodules. When G is a commutative group, this is the weight-space decomposition of a representation of the diagonalizable group D(G) = Spec R[G].

The independence and spanning statements above are packaged here by hand rather than through DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top, which needs a ring: over a semiring the lattice-theoretic independence is too weak, whereas the weight projections give the decomposition directly.

def TauCeti.Comodule.weightSubcomodule (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) : Subcomodule R (MonoidAlgebra R G) V

The g-weight submodule as a subcomodule: the decomposition is one of comodules, not merely of modules.

Equations

• TauCeti.Comodule.weightSubcomodule R G V g = { carrier := TauCeti.Comodule.weightSpace R G V g, coact_mem' := ⋯ }

@[simp]

theorem TauCeti.Comodule.weightSubcomodule_toSubmodule {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) : (weightSubcomodule R G V g).toSubmodule = weightSpace R G V g

@[simp]

theorem TauCeti.Comodule.mem_weightSubcomodule {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {g : G} {v : V} : v ∈ weightSubcomodule R G V g ↔ v ∈ weightSpace R G V g

Functoriality and finiteness

noncomputable def TauCeti.Comodule.Hom.ofMapWeightSpace {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {W : Type u_1} [AddCommMonoid W] [Module R W] [Comodule R (MonoidAlgebra R G) W] (f : V →ₗ[R] W) (hf : ∀ (g : G) {v : V}, v ∈ weightSpace R G V g → f v ∈ weightSpace R G W g) : Hom R (MonoidAlgebra R G) V W

A linear map between comodules over a monoid algebra is a comodule morphism if it preserves every weight space.

Equations

• TauCeti.Comodule.Hom.ofMapWeightSpace f hf = { toLinearMap := f, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.ofMapWeightSpace_toLinearMap {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {W : Type u_1} [AddCommMonoid W] [Module R W] [Comodule R (MonoidAlgebra R G) W] (f : V →ₗ[R] W) (hf : ∀ (g : G) {v : V}, v ∈ weightSpace R G V g → f v ∈ weightSpace R G W g) : (ofMapWeightSpace f hf).toLinearMap = f

@[simp]

theorem TauCeti.Comodule.Hom.map_weightProj {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {W : Type u_1} [AddCommMonoid W] [Module R W] [Comodule R (MonoidAlgebra R G) W] (f : Hom R (MonoidAlgebra R G) V W) (g : G) (v : V) : f ((weightProj R G V g) v) = (weightProj R G W g) (f v)

A comodule morphism over a monoid algebra commutes with every weight projection.

theorem TauCeti.Comodule.Hom.map_mem_weightSpace {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {W : Type u_1} [AddCommMonoid W] [Module R W] [Comodule R (MonoidAlgebra R G) W] (f : Hom R (MonoidAlgebra R G) V W) {g : G} {v : V} (hv : v ∈ weightSpace R G V g) : f v ∈ weightSpace R G W g

A morphism of comodules over R[G] sends the g-weight submodule into the g-weight submodule.

theorem TauCeti.Comodule.Hom.map_weightSpace_le {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] {W : Type u_1} [AddCommMonoid W] [Module R W] [Comodule R (MonoidAlgebra R G) W] (f : Hom R (MonoidAlgebra R G) V W) (g : G) : Submodule.map f.toLinearMap (weightSpace R G V g) ≤ weightSpace R G W g

A morphism of comodules over R[G] maps the g-weight submodule into the g-weight submodule.

theorem TauCeti.Comodule.weightProj_mem_subcomodule {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (N : Subcomodule R (MonoidAlgebra R G) V) (g : G) {v : V} (hv : v ∈ N) : (weightProj R G V g) v ∈ N

Every subcomodule over a monoid algebra is stable under the weight projections.

@[simp]

theorem TauCeti.Comodule.range_weightProj (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] (g : G) : (weightProj R G V g).range = weightSpace R G V g

The g-weight submodule is the range of the g-weight projection: the projection is idempotent with image the submodule it projects onto.

theorem TauCeti.Comodule.finite_setOf_weightSpace_ne_bot (R : Type u) (G : Type v) (V : Type w) [CommSemiring R] [AddCommMonoid V] [Module R V] [Comodule R (MonoidAlgebra R G) V] [Module.Finite R V] : {g : G | weightSpace R G V g ≠ ⊥}.Finite

A comodule over R[G] that is finitely generated as a module has only finitely many weights.

For a representation of the diagonalizable group D(G) this is the finiteness of its set of weights, and for the adjoint representation of an affine group scheme under a split torus it is the finiteness of the set of roots.

The action associated to an algebra map out of the monoid algebra

theorem TauCeti.Comodule.endOfPoint_tmul_of_mem_weightSpace {R : Type u} {G : Type v} {V : Type w} [CommSemiring R] [AddCommMonoid V] [Module R V] [Monoid G] [Comodule R (MonoidAlgebra R G) V] {A : Type u_1} [CommSemiring A] [Algebra R A] (f : MonoidAlgebra R G →ₐ[R] A) (a : A) {g : G} {v : V} (hv : v ∈ weightSpace R G V g) : (endOfPoint V f) (a ⊗ₜ[R] v) = (a * f (MonoidAlgebra.single g 1)) ⊗ₜ[R] v

The endomorphism associated to an algebra map out of R[G] acts by a scalar on each weight submodule. When G is a commutative group, these algebra maps are points of D(G), and the scalar f (single g 1) is the value of the character g at the point f.