Geometry of weight-unipotent subgroup schemes

For an integer weight w i on each coordinate of GL_N, the weight-unipotent subgroup has matrix entries fixed to the identity whenever w i ≤ w j. The remaining entries, indexed by pairs with w j < w i, are free polynomial coordinates. This file identifies its coordinate algebra with the polynomial algebra on those pairs.

The presentation is obtained directly from the determinant localization defining GL_N. The generic weight-unipotent matrix is block triangular with identity diagonal blocks, so its determinant is one and polynomial evaluation extends across the localization. The defining quotient relations then give mutually inverse maps.

The polynomial presentation proves that the represented subgroup is smooth over every commutative base ring and geometrically connected over a field. A forthcoming pointwise unipotence theorem will supply the remaining property required of the unipotent factor in the dynamic Levi decomposition.

Main declarations

• TauCeti.GeneralLinear.WeightUnipotentIndex: the free matrix coordinates w j < w i.
• TauCeti.GeneralLinear.weightUnipotentCoordinateAlgEquiv: the polynomial presentation of the weight-unipotent coordinate algebra.
• TauCeti.GeneralLinear.instSmoothWeightUnipotentCoordinateHopfAlgebra: smoothness over the base ring.
• geometricallyConnectedCommHopfAlgProperty_weightUnipotentCoordinateHopfAlgebra: geometric connectedness over a field.

References

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

This advances the dynamic approach to parabolics and Levi decomposition in Layer 7 of the ReductiveGroups roadmap.

@[reducible, inline]

abbrev TauCeti.GeneralLinear.WeightUnipotentIndex {N : ℕ} (w : Fin N → ℤ) : Type

Pairs indexing the matrix entries not fixed by the weight-unipotent relations.

Equations

• TauCeti.GeneralLinear.WeightUnipotentIndex w = { ij : Fin N × Fin N // w ij.2 < w ij.1 }

noncomputable def TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Matrix (Fin N) (Fin N) (MvPolynomial (WeightUnipotentIndex w) R)

The polynomial matrix whose free entries are precisely those strictly below the weight-block diagonal, with identity matrices on the diagonal blocks.

Equations

• TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix R w i j = if h : w j < w i then MvPolynomial.X ⟨(i, j), h⟩ else if i = j then 1 else 0

@[simp]

theorem TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix_apply_of_lt (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w j < w i) : weightUnipotentPolynomialGenericMatrix R w i j = MvPolynomial.X ⟨(i, j), hij⟩

A free entry of the polynomial weight-unipotent matrix is its corresponding variable.

@[simp]

theorem TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix_apply_of_le (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≤ w j) : weightUnipotentPolynomialGenericMatrix R w i j = 1 i j

An entry on or above the weight-block diagonal is the corresponding identity entry.

theorem TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix_blockTriangular (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : (weightUnipotentPolynomialGenericMatrix R w).BlockTriangular (⇑OrderDual.toDual ∘ w)

The polynomial weight-unipotent matrix is block triangular for the decreasing weight filtration.

@[simp]

theorem TauCeti.GeneralLinear.weightUnipotentPolynomialGenericMatrix_det (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : (weightUnipotentPolynomialGenericMatrix R w).det = 1

The determinant of the polynomial weight-unipotent matrix is one.

noncomputable def TauCeti.GeneralLinear.weightUnipotentCoordinateAlgEquiv (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : ↑(weightUnipotentCoordinateHopfAlgebra R w) ≃ₐ[R] MvPolynomial (WeightUnipotentIndex w) R

The weight-unipotent coordinate algebra is a polynomial algebra on the entries X_ij for which w j < w i.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.GeneralLinear.weightUnipotentCoordinateAlgEquiv_mk_genericMatrix_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (i j : Fin N) : (weightUnipotentCoordinateAlgEquiv R w) ((Ideal.Quotient.mkₐ R (weightUnipotentDefiningHopfIdeal R w).toIdeal) (genericMatrix R N i j)) = weightUnipotentPolynomialGenericMatrix R w i j

The polynomial presentation sends a canonical quotient generic-matrix entry to the corresponding polynomial weight-unipotent matrix entry.

@[simp]

theorem TauCeti.GeneralLinear.weightUnipotentCoordinateAlgEquiv_symm_X (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (ij : WeightUnipotentIndex w) : (weightUnipotentCoordinateAlgEquiv R w).symm (MvPolynomial.X ij) = (Ideal.Quotient.mkₐ R (weightUnipotentDefiningHopfIdeal R w).toIdeal) (genericMatrix R N (↑ij).1 (↑ij).2)

The inverse polynomial presentation sends a free variable to its quotient matrix entry.

instance TauCeti.GeneralLinear.instSmoothWeightUnipotentCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Algebra.Smooth R ↑(weightUnipotentCoordinateHopfAlgebra R w)

The weight-unipotent coordinate algebra is smooth over its base ring.

instance TauCeti.GeneralLinear.instIsDomainWeightUnipotentCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} [IsDomain R] (w : Fin N → ℤ) : IsDomain ↑(weightUnipotentCoordinateHopfAlgebra R w)

Over an integral domain, the weight-unipotent coordinate algebra is an integral domain.

theorem TauCeti.GeneralLinear.geometricallyConnectedCommHopfAlgProperty_weightUnipotentCoordinateHopfAlgebra {N : ℕ} (k : Type u) [Field k] (w : Fin N → ℤ) : geometricallyConnectedCommHopfAlgProperty k (weightUnipotentCoordinateHopfAlgebra k w)

The weight-unipotent subgroup is geometrically connected over every field.