Flags of upper-triangular comodules

Let M be a finite free comodule with basis b₀, ..., bₙ₋₁. Its coefficient matrix is upper triangular with diagonal c exactly when, for every i, the coaction of bᵢ is congruent to bᵢ ⊗ cᵢ modulo the span of the preceding basis vectors. Thus the standard basis flag is comodule-stable and its successive one-dimensional factors have weights cᵢ. The unitriangular case c = 1 says those factors are trivial.

This is the flag interface needed for the Kolchin inductions in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. Once such an induction supplies successive fixed vectors, the criterion here produces the upper-unitriangular coefficient matrix used to embed a faithful representation into Uₙ.

Main declarations

• TauCeti.Comodule.coefficientMatrix_isUpperTriangular_and_diag_iff: the quotient-by-preceding-span criterion for an upper-triangular coefficient matrix with prescribed diagonal.
• TauCeti.Comodule.coefficientMatrix_isUpperUnitriangular_iff: its unitriangular special case.
• TauCeti.Comodule.flagSubcomodule: the standard flag of an upper-triangular comodule, bundled as subcomodules.
• TauCeti.Comodule.quotient_mk_basis_ne_zero: each successive basis class is nonzero in the quotient by the preceding flag term.
• TauCeti.Comodule.quotientCoact_flagSubcomodule_mk_basis: each successive basis class has trivial coaction in that quotient.

References

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

theorem TauCeti.Comodule.coefficientMatrix_isUpperTriangular_and_diag_iff {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (c : Fin n → H) : ((coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), coefficientMatrix b i i = c i) ↔ ∀ (i : Fin n), (TensorProduct.map (b.flag i.castSucc).mkQ LinearMap.id) (coact (b i)) = Submodule.Quotient.mk (b i) ⊗ₜ[k] c i

A coefficient matrix is upper triangular with prescribed diagonal exactly when each basis vector has the prescribed coaction modulo the span of the preceding basis vectors.

theorem TauCeti.Comodule.coefficientMatrix_isUpperUnitriangular_iff {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [One H] (b : Module.Basis (Fin n) k M) : (coefficientMatrix b).IsUpperUnitriangular ↔ ∀ (i : Fin n), (TensorProduct.map (b.flag i.castSucc).mkQ LinearMap.id) (coact (b i)) = Submodule.Quotient.mk (b i) ⊗ₜ[k] 1

A coefficient matrix is upper unitriangular exactly when each basis vector is fixed by the coaction modulo the span of the preceding basis vectors.

def TauCeti.Comodule.flagSubcomodule {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) (r : Fin (n + 1)) : Subcomodule k H M

The initial spans of a basis with upper-triangular coefficient matrix, bundled as subcomodules.

Equations

• TauCeti.Comodule.flagSubcomodule b h r = b.coordinateSpanSubcomodule {i : Fin n | i.castSucc < r} ⋯

@[simp]

theorem TauCeti.Comodule.flagSubcomodule_toSubmodule {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) (r : Fin (n + 1)) : (flagSubcomodule b h r).toSubmodule = b.flag r

The underlying submodule of flagSubcomodule is the corresponding basis flag.

theorem TauCeti.Comodule.coact_basis_mem_flag {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) {i : Fin n} {r : Fin (n + 1)} (hir : i.castSucc < r) : coact (b i) ∈ (TensorProduct.map (b.flag r).subtype LinearMap.id).range

The coaction of a basis vector in a stable initial segment belongs to the tensor product of that initial segment with the coalgebra.

@[simp]

theorem TauCeti.Comodule.flagSubcomodule_zero {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) : flagSubcomodule b h 0 = ⊥

The first term of the bundled basis flag is the zero subcomodule.

@[simp]

theorem TauCeti.Comodule.flagSubcomodule_last {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) : flagSubcomodule b h (Fin.last n) = ⊤

The last term of the bundled basis flag is the full comodule.

theorem TauCeti.Comodule.flagSubcomodule_monotone {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperTriangular) : Monotone (flagSubcomodule b h)

The bundled basis flag is monotone.

theorem TauCeti.Comodule.flagSubcomodule_strictMono {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) [Nontrivial k] (h : (coefficientMatrix b).IsUpperTriangular) : StrictMono (flagSubcomodule b h)

The bundled basis flag is strictly monotone.

theorem TauCeti.Comodule.quotient_mk_basis_ne_zero {k : Type u} {M : Type w} {n : ℕ} [CommRing k] [AddCommGroup M] [Module k M] [Nontrivial k] (b : Module.Basis (Fin n) k M) (i : Fin n) : Submodule.Quotient.mk (b i) ≠ 0

A basis vector does not vanish in the quotient by the span of its predecessors.

theorem TauCeti.Comodule.quotientCoact_flagSubcomodule_mk_basis {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [AddCommMonoid H] [Module k H] [Coalgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [One H] (b : Module.Basis (Fin n) k M) (h : (coefficientMatrix b).IsUpperUnitriangular) (i : Fin n) : have N := flagSubcomodule b ⋯ i.castSucc; N.quotientCoact (Submodule.Quotient.mk (b i)) = Submodule.Quotient.mk (b i) ⊗ₜ[k] 1

In the quotient by the preceding term of an upper-unitriangular basis flag, the class of the next basis vector has trivial coaction.