Split flags for generated affine group schemes

A based representation preserves its decreasing weight filtration exactly when its coefficient matrix is block triangular. This file expresses the same condition for the closed subgroup scheme generated by a family of morphisms: the image of the weight-parabolic ideal under the representation's coordinate morphism lies in the family's common-kernel Hopf ideal exactly when every member of the family has block-triangular coefficient matrix.

This is entirely scheme theoretic. It makes no assertion about density of algebra-valued points. Related criteria for tensors preserved by generated subgroup schemes are developed in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Generated.Preserves.

Main declaration

• TauCeti.Comodule.weightParabolic_map_coordinateBialgHom_le_commonKernel_iff_blockTriangular: a family of generators preserves a split weighted flag exactly when the generated closed subgroup scheme does.
• TauCeti.Comodule.coefficientMatrix_commonKernelQuotient_blockTriangular: the representation corestricted to the generated group's coordinate algebra has block-triangular coefficient matrix.

theorem TauCeti.Comodule.weightParabolic_map_coordinateBialgHom_le_commonKernel_iff_blockTriangular {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] {n : ℕ} {ι : Type x} {K : ι → CommHopfAlgCat R} (f : (a : ι) → H ⟶ K a) (b : Module.Basis (Fin n) R M) (weight : Fin n → ℤ) : (GeneralLinear.weightParabolicDefiningHopfIdeal R weight).map (coordinateBialgHom b) ≤ CommHopfAlgCat.commonKernelHopfIdeal f ↔ ∀ (a : ι), ((coefficientMatrix b).map ⇑(CommHopfAlgCat.Hom.hom (f a))).BlockTriangular (⇑OrderDual.toDual ∘ weight)

The image of the weight-parabolic ideal under a representation's coordinate morphism lies in the common-kernel ideal of a family precisely when every member of the family makes the coefficient matrix block triangular.

Contravariantly, the right side says that every generating subgroup scheme preserves the split decreasing weight filtration, while the left side says the closed subgroup scheme they generate does so.

theorem TauCeti.Comodule.coefficientMatrix_commonKernelQuotient_blockTriangular {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] {n : ℕ} {ι : Type x} {K : ι → CommHopfAlgCat R} (f : (a : ι) → H ⟶ K a) (b : Module.Basis (Fin n) R M) (weight : Fin n → ℤ) (h : ∀ (a : ι), ((coefficientMatrix b).map ⇑(CommHopfAlgCat.Hom.hom (f a))).BlockTriangular (⇑OrderDual.toDual ∘ weight)) : have J := CommHopfAlgCat.commonKernelHopfIdeal f; (coefficientMatrix b).BlockTriangular (⇑OrderDual.toDual ∘ weight)

If every member of a family has block-triangular coefficient matrix, then so does the representation corestricted to the common-kernel quotient, the coordinate algebra of the closed subgroup scheme generated by that family. Consequently, Module.Basis.weightCoordinateSpanSubcomodule constructs every step of the split decreasing weight filtration as a subcomodule over the generated group.