Building upper-unitriangular bases from fixed vectors

Suppose every nonzero finite-dimensional comodule over a coalgebra with a distinguished element 1 has a nonzero fixed vector, that is, a vector v with coaction v ↦ v ⊗ 1. Then every finite-dimensional comodule has a basis whose coefficient matrix is upper unitriangular: this is the weight-vector induction of TauCeti.Algebra.Coalgebra.Comodule.Flag.Triangular with the weights confined to {1}.

This is the fixed-vector case of the induction common to the Kolchin arguments in Layer 5 of the ReductiveGroups roadmap. Lie–Kolchin supplies eigenlines for solvable groups; for a unipotent group every resulting character is trivial, so the lines are fixed. The theorem here turns that fixed-vector statement into the complete flag needed to embed a faithful representation into an upper-unitriangular group.

Main declarations

• TauCeti.Comodule.HasNonzeroFixedVector: a comodule contains a nonzero vector with coaction v ↦ v ⊗ 1.
• TauCeti.Comodule.hasNonzeroFixedVector_iff_fixedSubcomodule_ne_bot: that happens exactly when the fixed subcomodule is nonzero.
• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperUnitriangular_of_fixed_vectors: if every nonzero finite-dimensional comodule has such a vector, every finite-dimensional comodule admits an upper-unitriangular basis.

References

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

def TauCeti.Comodule.HasNonzeroFixedVector (k : Type u) (H : Type v) (M : Type w) [Field k] [AddCommGroup H] [Module k H] [Coalgebra k H] [One H] [AddCommGroup M] [Module k M] [Comodule k H M] : Prop

A comodule has a nonzero fixed vector if some nonzero v has coaction v ⊗ 1.

For the comodule corresponding to a group representation, this says that the represented group fixes v.

Equations

• TauCeti.Comodule.HasNonzeroFixedVector k H M = ∃ (v : M), v ≠ 0 ∧ TauCeti.Comodule.coact v = v ⊗ₜ[k] 1

@[simp]

theorem TauCeti.Comodule.hasNonzeroFixedVector_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [AddCommGroup H] [Module k H] [Coalgebra k H] [One H] [AddCommGroup M] [Module k M] [Comodule k H M] : HasNonzeroFixedVector k H M ↔ ∃ (v : M), v ≠ 0 ∧ coact v = v ⊗ₜ[k] 1

The defining characterization of a nonzero fixed vector.

theorem TauCeti.Comodule.hasNonzeroFixedVector_iff_fixedSubcomodule_ne_bot {k : Type u} {H : Type v} {M : Type w} [Field k] [AddCommGroup H] [Module k H] [Coalgebra k H] [One H] [AddCommGroup M] [Module k M] [Comodule k H M] : HasNonzeroFixedVector k H M ↔ fixedSubcomodule k H M ≠ ⊥

A comodule has a nonzero fixed vector exactly when its fixed subcomodule is nonzero.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperUnitriangular_of_fixed_vectors {k : Type u} {H : Type v} {M : Type w} [Field k] [AddCommGroup H] [Module k H] [Coalgebra k H] [One H] [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] (hfixed : ∀ (V : Type w) [inst : AddCommGroup V] [inst_1 : Module k V] [inst_2 : Comodule k H V] [FiniteDimensional k V] [Nontrivial V], HasNonzeroFixedVector k H V) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperUnitriangular

If every nonzero finite-dimensional H-comodule has a nonzero fixed vector, then every finite-dimensional H-comodule has a basis with upper-unitriangular coefficient matrix.

The hypothesis is deliberately uniform in the comodule: the induction applies it to successive quotients. The conclusion allows an arbitrary finite index n; the exhibited basis itself certifies that n is the dimension of M.