Weight spaces of a comodule

Let M be a comodule over a coalgebra C over a commutative semiring. For a group-like element c of C, its weight space is the submodule of vectors whose coaction is m ↦ m ⊗ c. This file packages that submodule and its elementary functorial API. Over a domain, when C is projective and M is torsion-free, it proves that the weight spaces belonging to distinct group-like elements are independent. Consequently a Noetherian comodule has only finitely many nonzero weight spaces.

The independence proof reads a coaction through all linear functionals on C. The c-weight space is the joint eigenspace of the component endomorphisms Comodule.coactComponent φ, with eigenvalue function φ ↦ φ c. Linear functionals separate points when C is projective, so distinct group-like elements give distinct joint eigenvalue functions.

Unlike the weight decomposition for a monoid algebra, these weight spaces need not span an arbitrary comodule. Their finite nonzero support can be used to define permutation actions on weights in Lie--Kolchin arguments.

Main declarations

• GroupLike.weightSpace: the weight space belonging to a group-like element.
• GroupLike.weightSubcomodule: the weight space as a subcomodule.
• TauCeti.Subcomodule.existsUnique_le_groupLikeWeightSpace_of_finrank_eq_one: a line subcomodule lies in the weight space of a unique group-like element.
• TauCeti.Comodule.iSupIndep_groupLikeWeightSpace: distinct group-like weight spaces are independent.
• TauCeti.Comodule.finite_setOf_groupLikeWeightSpace_ne_bot: a Noetherian comodule has only finitely many nonzero group-like weight spaces.
• TauCeti.Comodule.NonzeroGroupLikeWeight: the group-like elements with nonzero weight space.
• TauCeti.Comodule.natCard_nonzeroGroupLikeWeights_le_finrank: the number of nonzero weight spaces is at most the dimension of the comodule.
• TauCeti.Comodule.hasNonzeroWeightVector_iff_exists_groupLikeWeightSpace_ne_bot: nonzero weight vectors are exactly nontrivial group-like weight spaces.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Theorem 6.3.1.

def GroupLike.weightSpace {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (c : GroupLike R C) : Submodule R M

The weight space of a group-like element c consists of the vectors with coaction m ↦ m ⊗ c.

Equations

• c.weightSpace = TauCeti.Comodule.coact.eqLocus ((TensorProduct.mk R M C).flip ↑c)

@[simp]

theorem GroupLike.mem_weightSpace {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {c : GroupLike R C} {m : M} : m ∈ c.weightSpace ↔ TauCeti.Comodule.coact m = m ⊗ₜ[R] ↑c

Membership in a group-like weight space is the corresponding coaction equation.

def GroupLike.weightSubcomodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (c : GroupLike R C) : TauCeti.Subcomodule R C M

A group-like weight space, regarded as a subcomodule.

Equations

• c.weightSubcomodule = TauCeti.Subcomodule.ofSubmodule c.weightSpace ⋯

@[simp]

theorem GroupLike.weightSubcomodule_toSubmodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] (c : GroupLike R C) : c.weightSubcomodule.toSubmodule = c.weightSpace

The underlying submodule of the group-like weight subcomodule is its weight space.

@[simp]

theorem GroupLike.mem_weightSubcomodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R C M] {c : GroupLike R C} {m : M} : m ∈ c.weightSubcomodule ↔ TauCeti.Comodule.coact m = m ⊗ₜ[R] ↑c

Membership in the group-like weight subcomodule is the corresponding coaction equation.

@[reducible, inline]

abbrev TauCeti.Comodule.NonzeroGroupLikeWeight (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] : Type v

The group-like elements whose weight space in a comodule is nonzero.

Equations

• TauCeti.Comodule.NonzeroGroupLikeWeight R C M = { c : GroupLike R C // c.weightSpace ≠ ⊥ }

theorem TauCeti.Comodule.Hom.map_mem_groupLikeWeightSpace {R : Type u} {C : Type v} {M : Type w} {N : Type x} [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) {c : GroupLike R C} {m : M} (hm : m ∈ c.weightSpace) : f m ∈ c.weightSpace

A comodule morphism preserves every group-like weight space.

theorem TauCeti.Comodule.Hom.map_groupLikeWeightSpace_le {R : Type u} {C : Type v} {M : Type w} {N : Type x} [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) (c : GroupLike R C) : Submodule.map f.toLinearMap c.weightSpace ≤ c.weightSpace

A comodule morphism maps each group-like weight space into the same weight space.

theorem TauCeti.Comodule.hasNonzeroWeightVector_iff_exists_groupLikeWeightSpace_ne_bot {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] : HasNonzeroWeightVector R C M ↔ ∃ (c : GroupLike R C), c.weightSpace ≠ ⊥

A comodule has a nonzero weight vector exactly when one of its group-like weight spaces is nonzero.

theorem TauCeti.Comodule.mem_groupLikeWeightSpace_iff_forall_coactComponent_eq_smul {k : Type u} {C : Type v} {M : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommMonoid M] [Module k M] [Comodule k C M] {c : GroupLike k C} {m : M} : m ∈ c.weightSpace ↔ ∀ (φ : Module.Dual k C), (coactComponent φ) m = φ ↑c • m

A vector has weight c exactly when every component of its coaction has eigenvalue obtained by evaluating the component functional at c.

theorem TauCeti.Subcomodule.existsUnique_le_groupLikeWeightSpace_of_finrank_eq_one {k : Type u_1} {C : Type u_2} {M : Type u_3} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (L : Subcomodule k C M) (hL : Module.finrank k ↥L.toSubmodule = 1) : ∃! χ : GroupLike k C, L.toSubmodule ≤ χ.weightSpace

A one-dimensional subcomodule lies in the weight space of a unique group-like element. For a coordinate Hopf algebra, this is the character by which the group acts on the line.

theorem GroupLike.weightSpace_eq_iInf_eigenspace {k : Type u} {C : Type v} {M : Type w} [CommRing k] [AddCommGroup C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommGroup M] [Module k M] [TauCeti.Comodule k C M] (c : GroupLike k C) : c.weightSpace = ⨅ (φ : Module.Dual k C), Module.End.eigenspace (TauCeti.Comodule.coactComponent φ) (φ ↑c)

A group-like weight space is the joint eigenspace of all components of the coaction.

theorem TauCeti.Comodule.iSupIndep_groupLikeWeightSpace {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommGroup M] [Module k M] [Module.IsTorsionFree k M] [Comodule k C M] : iSupIndep GroupLike.weightSpace

The group-like weight spaces of a torsion-free comodule over a domain are supremum-independent.

theorem TauCeti.Comodule.finite_setOf_groupLikeWeightSpace_ne_bot_of_fg {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommGroup M] [Module k M] [Module.IsTorsionFree k M] [Comodule k C M] (hfg : (⨆ (c : GroupLike k C), c.weightSpace).FG) : {c : GroupLike k C | c.weightSpace ≠ ⊥}.Finite

A family of group-like weight spaces with finitely generated supremum has finite support.

theorem TauCeti.Comodule.finite_setOf_groupLikeWeightSpace_ne_bot {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommGroup M] [Module k M] [Module.IsTorsionFree k M] [Comodule k C M] [IsNoetherian k M] : {c : GroupLike k C | c.weightSpace ≠ ⊥}.Finite

A Noetherian comodule has only finitely many nonzero group-like weight spaces.

instance TauCeti.Comodule.instFiniteNonzeroGroupLikeWeight {k : Type u} {C : Type v} {M : Type w} [CommRing k] [IsDomain k] [AddCommGroup C] [Module k C] [Coalgebra k C] [Module.Projective k C] [AddCommGroup M] [Module k M] [Module.IsTorsionFree k M] [Comodule k C M] [IsNoetherian k M] : Finite (NonzeroGroupLikeWeight k C M)

The nonzero group-like weights of a Noetherian comodule form a finite type.

theorem TauCeti.Comodule.natCard_nonzeroGroupLikeWeights_le_finrank {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] [FiniteDimensional k M] : Nat.card (NonzeroGroupLikeWeight k C M) ≤ Module.finrank k M

The number of nonzero group-like weight spaces of a finite-dimensional comodule is at most the dimension of the comodule.