Weight vectors of a comodule

A weight vector of a comodule M over a coalgebra C is a vector v whose coaction is v ↦ v ⊗ c for a single element c of C. Over a field, this is equivalent to the line it spans being a subcomodule. When C is the coordinate Hopf algebra of an affine group, this says that every point of the group scales v, by the value it takes on c.

Over a field, the weight of a nonzero weight vector is automatically group-like: the counit law forces ε c = 1 and coassociativity forces Δ c = c ⊗ c, because a nonzero vector of a vector space is detected by a linear functional. So a one-dimensional subcomodule of a comodule over a field is specified by a group-like element. When C is the coordinate Hopf algebra of an affine group, that group-like element is a character, so there is no need to carry group-likeness as a hypothesis. Over a general commutative semiring, HasNonzeroWeightVector instead explicitly requires its exhibited weight to be group-like.

Weight vectors are the eigenvector form of the fixed vectors of TauCeti.Algebra.Coalgebra.Comodule.Fixed: a fixed vector is a weight vector of weight 1. They are what the Lie--Kolchin argument produces for a connected solvable group, where fixed vectors are unavailable, and the flag induction of TauCeti.Algebra.Coalgebra.Comodule.Flag.Triangular turns them into a complete invariant flag.

Main declarations

• TauCeti.Comodule.HasNonzeroWeightVector: a comodule contains a nonzero weight vector.
• TauCeti.Comodule.isGroupLikeElem_of_coact_eq_tmul: the weight of a nonzero weight vector is group-like.
• TauCeti.Comodule.eq_of_coact_eq_tmul: the weight of a nonzero weight vector is unique.
• TauCeti.Comodule.exists_isGroupLikeElem_coact_eq_tmul_of_toSubmodule_eq_span: a subcomodule spanned by a single nonzero vector exhibits it as a weight vector.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §§2.4 and 6.3.

def TauCeti.Comodule.HasNonzeroWeightVector (k : Type u) (C : Type v) (M : Type w) [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid M] [Module k M] [Comodule k C M] : Prop

A comodule has a nonzero weight vector if some nonzero v has coaction v ⊗ c for a group-like c.

When C is the coordinate Hopf algebra of an affine group, this says that the group acts on the line spanned by v through the character corresponding to c.

Equations

• TauCeti.Comodule.HasNonzeroWeightVector k C M = ∃ (v : M) (c : C), v ≠ 0 ∧ IsGroupLikeElem k c ∧ TauCeti.Comodule.coact v = v ⊗ₜ[k] c

@[simp]

theorem TauCeti.Comodule.hasNonzeroWeightVector_iff {k : Type u} {C : Type v} {M : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid M] [Module k M] [Comodule k C M] : HasNonzeroWeightVector k C M ↔ ∃ (v : M) (c : C), v ≠ 0 ∧ IsGroupLikeElem k c ∧ coact v = v ⊗ₜ[k] c

The defining characterization of a nonzero weight vector.

theorem TauCeti.Comodule.isGroupLikeElem_of_coact_eq_tmul {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] {v : M} (hv : v ≠ 0) {c : C} (h : coact v = v ⊗ₜ[k] c) : IsGroupLikeElem k c

The weight of a nonzero weight vector is a group-like element.

theorem TauCeti.Comodule.eq_of_coact_eq_tmul {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] {v : M} (hv : v ≠ 0) {c d : C} (hc : coact v = v ⊗ₜ[k] c) (hd : coact v = v ⊗ₜ[k] d) : c = d

The weight of a nonzero weight vector is unique.

theorem TauCeti.Comodule.coact_eq_tmul_of_mem_span {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] {v : M} {c : C} (h : coact v = v ⊗ₜ[k] c) {x : M} (hx : x ∈ k ∙ v) : coact x = x ⊗ₜ[k] c

Every vector of a line spanned by a weight vector is a weight vector of the same weight.

theorem TauCeti.Comodule.exists_isGroupLikeElem_coact_eq_tmul_of_mem_range {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] {v : M} (hv : v ≠ 0) (h : coact v ∈ (TensorProduct.map (k ∙ v).subtype LinearMap.id).range) : ∃ (c : C), IsGroupLikeElem k c ∧ coact v = v ⊗ₜ[k] c

A vector whose coaction lies in the tensor product of the line it spans with the coalgebra is a weight vector, and its weight is group-like.

theorem TauCeti.Comodule.exists_isGroupLikeElem_coact_eq_tmul_of_toSubmodule_eq_span {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) {v : M} (hv : v ≠ 0) (hN : N.toSubmodule = k ∙ v) : ∃ (c : C), IsGroupLikeElem k c ∧ coact v = v ⊗ₜ[k] c

A subcomodule spanned by a single nonzero vector exhibits that vector as a weight vector.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_toSubmodule_eq_span {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) {v : M} (hv : v ≠ 0) (hN : N.toSubmodule = k ∙ v) : HasNonzeroWeightVector k C M

A subcomodule spanned by a single nonzero vector makes the ambient comodule have a nonzero weight vector.