Upper-triangular comodule structures and extensions

An extension of upper-triangular comodules is again upper triangular. More explicitly, let N be a subcomodule of M. A basis of N and a basis of M ⧸ N combine, using Mathlib's Module.Basis.sumQuot, into a basis of M. If the coefficient matrices on the subcomodule and quotient are upper triangular, then the combined coefficient matrix is upper triangular, and its diagonal is the concatenation of theirs; in particular unitriangularity is inherited too.

The coefficient matrix has the expected block form. Its diagonal blocks are the coefficient matrices of N and M ⧸ N, its lower-left block is zero because N is stable, and its upper-right block records the extension class.

This is the extension step needed by the Kolchin inductions in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. A weight line supplies the first diagonal block; applying the induction hypothesis to the quotient and this file to the resulting extension constructs the complete invariant flag.

Main declarations

• TauCeti.Comodule.extensionBasis: the basis of a comodule obtained from bases of a subcomodule and its quotient.
• TauCeti.Comodule.coefficientMatrix_extensionBasis_castAdd_castAdd: the subcomodule diagonal block.
• TauCeti.Comodule.coefficientMatrix_extensionBasis_natAdd_natAdd: the quotient diagonal block.
• TauCeti.Comodule.coefficientMatrix_extensionBasis_natAdd_castAdd: the vanishing lower-left block.
• TauCeti.Comodule.coefficientMatrix_extensionBasis_isUpperTriangular: closure of upper-triangular comodule structures under extensions.
• TauCeti.Comodule.coefficientMatrix_extensionBasis_isUpperUnitriangular: its unitriangular refinement.

References

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

noncomputable def TauCeti.Comodule.extensionBasis {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) : Module.Basis (Fin (m + n)) k M

The basis of a comodule obtained by putting a basis of a subcomodule before chosen lifts of a basis of the quotient. The construction is Mathlib's Module.Basis.sumQuot, reindexed by the standard equivalence Fin m ⊕ Fin n ≃ Fin (m + n).

Equations

• TauCeti.Comodule.extensionBasis N bN bQ = TauCeti.extensionBasis N.toSubmodule (TauCeti.Comodule.toSubmoduleBasis✝ N bN) bQ

@[simp]

theorem TauCeti.Comodule.extensionBasis_castAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (i : Fin m) : (extensionBasis N bN bQ) (Fin.castAdd n i) = ↑(bN i)

On the first block, extensionBasis is the given basis of the subcomodule.

@[simp]

theorem TauCeti.Comodule.extensionBasis_natAdd_mkQ {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (j : Fin n) : Submodule.Quotient.mk ((extensionBasis N bN bQ) (Fin.natAdd m j)) = bQ j

On the second block, the quotient classes of extensionBasis are the given quotient basis.

@[simp]

theorem TauCeti.Comodule.extensionBasis_repr_castAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (x : ↥N) (i : Fin m) : ((extensionBasis N bN bQ).repr ↑x) (Fin.castAdd n i) = (bN.repr x) i

The first-block coordinates of an element of the subcomodule in extensionBasis are its coordinates in the given subcomodule basis.

@[simp]

theorem TauCeti.Comodule.extensionBasis_repr_natAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (x : M) (j : Fin n) : ((extensionBasis N bN bQ).repr x) (Fin.natAdd m j) = (bQ.repr (N.toSubmodule.mkQ x)) j

The second-block coordinates in extensionBasis are the coordinates of the quotient class.

@[simp]

theorem TauCeti.Comodule.coefficientMatrix_extensionBasis_castAdd_castAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (i j : Fin m) : coefficientMatrix (extensionBasis N bN bQ) (Fin.castAdd n i) (Fin.castAdd n j) = coefficientMatrix bN i j

The subcomodule diagonal block of the combined coefficient matrix is the coefficient matrix in the given subcomodule basis.

@[simp]

theorem TauCeti.Comodule.coefficientMatrix_extensionBasis_natAdd_castAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (i : Fin n) (j : Fin m) : coefficientMatrix (extensionBasis N bN bQ) (Fin.natAdd m i) (Fin.castAdd n j) = 0

The lower-left block of the combined coefficient matrix vanishes. This is the matrix form of stability of the subcomodule.

@[simp]

theorem TauCeti.Comodule.coefficientMatrix_extensionBasis_natAdd_natAdd {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (i j : Fin n) : coefficientMatrix (extensionBasis N bN bQ) (Fin.natAdd m i) (Fin.natAdd m j) = coefficientMatrix bQ i j

The quotient diagonal block of the combined coefficient matrix is the coefficient matrix in the given quotient basis.

theorem TauCeti.Comodule.coefficientMatrix_extensionBasis_isUpperTriangular {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (hN : (coefficientMatrix bN).IsUpperTriangular) (hQ : (coefficientMatrix bQ).IsUpperTriangular) : (coefficientMatrix (extensionBasis N bN bQ)).IsUpperTriangular

If the induced coefficient matrices on a subcomodule and its quotient are upper triangular, then the coefficient matrix on their combined basis is upper triangular.

theorem TauCeti.Comodule.coefficientMatrix_extensionBasis_isUpperUnitriangular {k : Type u} {C : Type v} {M : Type w} {m n : ℕ} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [Comodule k C M] [One C] (N : Subcomodule k C M) (bN : Module.Basis (Fin m) k ↥N) (bQ : Module.Basis (Fin n) k (M ⧸ N.toSubmodule)) (hN : (coefficientMatrix bN).IsUpperUnitriangular) (hQ : (coefficientMatrix bQ).IsUpperUnitriangular) : (coefficientMatrix (extensionBasis N bN bQ)).IsUpperUnitriangular

If the induced coefficient matrices on a subcomodule and its quotient are upper unitriangular, then the coefficient matrix on their combined basis is upper unitriangular.