Dynamic subgroups of the general linear group from weights

An integer weight w i on each coordinate of GL_N defines the cocharacter

lambda_w(t) = diag(t ^ w(0), ..., t ^ w(N - 1)).

Conjugation multiplies the (i,j) matrix entry by t ^ (w i - w j). Consequently its dynamic parabolic consists exactly of matrices that are block triangular for the weight filtration: an entry vanishes whenever w i < w j. The dynamic limit deletes the entries between distinct weight spaces. This also identifies the Levi subgroup with the block diagonal matrices and the dynamic unipotent subgroup with the block-triangular matrices acting as the identity on every associated-graded weight space.

The results hold over every commutative base ring and every commutative value algebra. In particular they do not infer the vanishing of a negative Laurent coefficient by cancellation; the coefficient is read directly, so zero divisors cause no problem.

Main declarations

• TauCeti.GeneralLinear.weightCocharacter: the cocharacter attached to integer weights.
• TauCeti.GeneralLinear.Dynamic.mem_parabolic_weightCocharacter_iff: its dynamic parabolic is the block-triangular subgroup for the weight filtration.
• TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_limit_weightCocharacter_apply: its limit keeps exactly the entries between equal-weight coordinates.
• TauCeti.GeneralLinear.Dynamic.mem_levi_weightCocharacter_iff: its Levi is block diagonal.
• TauCeti.GeneralLinear.Dynamic.mem_unipotent_weightCocharacter_iff: its unipotent subgroup consists of block-triangular matrices acting as the identity on the associated graded.

References

• G. R. Kempf, Instability in invariant theory, Annals of Mathematics 108 (1978), §2.
• J. S. Milne, Algebraic Groups (2017), Chapter 13.

This supplies the higher-rank block-cocharacter calculation requested by the dynamic-parabolic route in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

theorem TauCeti.GeneralLinear.Dynamic.pointsHom_weightCocharacter {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (t : Aˣ) : (Cocharacter.pointsHom A (weightCocharacter w)) t = (weightCocharacterPoints w) (MultiplicativeGroup.pointsMulEquiv.symm t)

The abstract cocharacter action agrees with the concrete weight cocharacter on points.

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_pointsHom_weightCocharacter {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (t : Aˣ) : (pointsMulEquiv N) ((Cocharacter.pointsHom A (weightCocharacter w)) t) = diagGL ((weightDiagonalUnits w) t)

The cocharacter with weights w sends t to diag(t ^ w i).

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_conjugate_weightCocharacter {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) : (pointsMulEquiv N) ((Cocharacter.conjugate A (weightCocharacter w)) g) = diagGL ((weightDiagonalUnits w) (MultiplicativeGroup.genericUnit A)) * (Matrix.GeneralLinearGroup.map ↑(IsScalarTower.toAlgHom R A (LaurentPolynomial A))) ((pointsMulEquiv N) g) * (diagGL ((weightDiagonalUnits w) (MultiplicativeGroup.genericUnit A)))⁻¹

Conjugation by the weight cocharacter is conjugation by the diagonal matrix diag(T ^ w i).

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_conjugate_weightCocharacter_apply {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) (i j : Fin N) : ↑((pointsMulEquiv N) ((Cocharacter.conjugate A (weightCocharacter w)) g)) i j = LaurentPolynomial.C (↑((pointsMulEquiv N) g) i j) * LaurentPolynomial.T (w i - w j)

The (i,j) entry of conjugation by the weight cocharacter is g_ij * T ^ (w i - w j).

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_parabolic_weightCocharacter_iff {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) : g ∈ Cocharacter.parabolic A (weightCocharacter w) ↔ (↑((pointsMulEquiv N) g)).BlockTriangular (⇑OrderDual.toDual ∘ w)

Membership in the dynamic parabolic for the weight cocharacter is exactly block triangularity for the decreasing weight filtration. Equivalently, g_ij = 0 whenever w i < w j.

theorem TauCeti.GeneralLinear.Dynamic.pointsMulEquiv_limit_weightCocharacter_apply {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) (hg : g ∈ Cocharacter.parabolic A (weightCocharacter w)) (i j : Fin N) : ↑((pointsMulEquiv N) ((Cocharacter.limit A (weightCocharacter w)) ⟨g, hg⟩)) i j = if w i = w j then ↑((pointsMulEquiv N) g) i j else 0

The dynamic limit for a weight cocharacter keeps an entry exactly when its row and column have equal weight.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_levi_weightCocharacter_iff {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) : g ∈ Cocharacter.levi A (weightCocharacter w) ↔ ∀ (i j : Fin N), w i ≠ w j → ↑((pointsMulEquiv N) g) i j = 0

Membership in the dynamic Levi subgroup for a weight cocharacter means preserving every weight space: matrix entries between distinct weights vanish.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_unipotent_weightCocharacter_iff {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (g : WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)) : g ∈ Cocharacter.unipotent A (weightCocharacter w) ↔ (↑((pointsMulEquiv N) g)).BlockTriangular (⇑OrderDual.toDual ∘ w) ∧ ∀ (i j : Fin N), w i = w j → ↑((pointsMulEquiv N) g) i j = 1 i j

Membership in the dynamic unipotent subgroup for a weight cocharacter means block triangularity together with identity action on each associated-graded weight space.