Comodules with a group-like basis

A basis b of a module M together with a family c of group-like elements of a coalgebra C determines a right C-comodule structure on M, namely the linear extension of

b x ↦ b x ⊗ c x.

The comodule axioms hold entry by entry: coassociativity is Δ(c x) = c x ⊗ c x and the counit law is ε(c x) = 1, which is exactly what group-likeness says. Its coefficient matrix in the basis b is the diagonal matrix of the c x.

When C = R[G] is the coordinate Hopf algebra of a diagonalizable group D(G) and c x = single (wt x) 1 for a weight function wt, this is the representation of D(G) acting on the x-th basis vector through the character wt x; the basis vectors then lie in the weight submodules of TauCeti.Algebra.Coalgebra.Comodule.MonoidAlgebra.Basic. This construction is complementary to the weight decomposition proved there: that file splits a comodule into weight spaces, while this one builds a comodule from a basis equipped with a prescribed weight function.

Main declarations

• TauCeti.Comodule.ofGroupLike: the comodule structure with prescribed group-like eigenvalues on a basis.
• TauCeti.Comodule.ofWeights: its specialization to a group algebra, given by a weight function.

Main results

• TauCeti.Comodule.coefficientMatrix_ofGroupLike: the coefficient matrix of a group-like basis is diagonal.
• TauCeti.Comodule.basis_mem_weightSpace_ofWeights: the x-th basis vector has weight wt x.
• TauCeti.Comodule.weightProj_ofWeights_eq: for distinct weights, weight projection extracts the corresponding basis coordinate.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• J. S. Milne, Algebraic Groups (2017), §12.c.

The comodule attached to a group-like basis

@[instance_reducible]

noncomputable def TauCeti.Comodule.ofGroupLike {R : Type u} {C : Type v} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] (b : Module.Basis η R M) (c : η → C) (hc : ∀ (x : η), IsGroupLikeElem R (c x)) : Comodule R C M

The right C-comodule structure on a free module which sends each basis vector b x to b x ⊗ c x, for a prescribed family c of group-like elements of C.

Group-likeness of c x is exactly the pair of comodule axioms evaluated at b x.

Equations

• TauCeti.Comodule.ofGroupLike b c hc = { coact := (b.constr R) fun (x : η) => b x ⊗ₜ[R] c x, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.ofGroupLike_coact_basis {R : Type u} {C : Type v} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] (b : Module.Basis η R M) (c : η → C) (hc : ∀ (x : η), IsGroupLikeElem R (c x)) (x : η) : coact (b x) = b x ⊗ₜ[R] c x

The coaction of ofGroupLike on a basis vector.

theorem TauCeti.Comodule.ofGroupLike_coact {R : Type u} {C : Type v} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] (b : Module.Basis η R M) (c : η → C) (hc : ∀ (x : η), IsGroupLikeElem R (c x)) (m : M) : coact m = (b.repr m).sum fun (x : η) (r : R) => r • b x ⊗ₜ[R] c x

The coaction of ofGroupLike on an arbitrary vector expands its coordinates.

theorem TauCeti.Comodule.coefficientMatrix_ofGroupLike {R : Type u} {C : Type v} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [DecidableEq η] (b : Module.Basis η R M) (c : η → C) (hc : ∀ (x : η), IsGroupLikeElem R (c x)) : coefficientMatrix b = Matrix.diagonal c

The coefficient matrix of a group-like basis is diagonal, with the prescribed group-like elements down the diagonal.

Weights over a group algebra

@[instance_reducible]

noncomputable def TauCeti.Comodule.ofWeights {R : Type u} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] {G : Type u_1} (b : Module.Basis η R M) (wt : η → G) : Comodule R (MonoidAlgebra R G) M

The right R[G]-comodule structure on a free module determined by a weight function on a basis: the basis vector b x is acted on through the character wt x.

This is the representation of the diagonalizable group D(G) which is diagonal in the basis b with the prescribed weights.

Equations

• TauCeti.Comodule.ofWeights b wt = TauCeti.Comodule.ofGroupLike b (fun (x : η) => MonoidAlgebra.single (wt x) 1) ⋯

theorem TauCeti.Comodule.ofWeights_coact_basis {R : Type u} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] {G : Type u_1} (b : Module.Basis η R M) (wt : η → G) (x : η) : coact (b x) = b x ⊗ₜ[R] MonoidAlgebra.single (wt x) 1

The coaction of ofWeights on a basis vector.

This is not a simp lemma: ofWeights unfolds to ofGroupLike, whose corresponding lemma is the simp normal form.

theorem TauCeti.Comodule.basis_mem_weightSpace_ofWeights {R : Type u} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] {G : Type u_1} (b : Module.Basis η R M) (wt : η → G) (x : η) : b x ∈ weightSpace R G M (wt x)

The x-th basis vector of ofWeights has weight wt x.

@[simp]

theorem TauCeti.Comodule.weightProj_ofWeights_eq {R : Type u} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] {G : Type u_1} (b : Module.Basis η R M) (wt : η → G) (hwt : Function.Injective wt) (x : η) (m : M) : (weightProj R G M (wt x)) m = (b.repr m) x • b x

In a basis with pairwise distinct weights, projection to the weight of a basis vector extracts exactly that basis coordinate.

theorem TauCeti.Comodule.coefficientMatrix_ofWeights {R : Type u} {M : Type w} {η : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] {G : Type u_1} [DecidableEq η] (b : Module.Basis η R M) (wt : η → G) : coefficientMatrix b = Matrix.diagonal fun (x : η) => MonoidAlgebra.single (wt x) 1

The coefficient matrix of ofWeights is the diagonal matrix of the characters.