Weight-unipotent subgroup schemes of the general linear group

An integer weight w i on each coordinate of GL_N defines a decreasing filtration. The unipotent subgroup attached to this filtration consists of the invertible matrices which are block triangular and induce the identity on every associated-graded weight space. Equivalently, its (i,j) entry is the identity-matrix entry whenever w i ≤ w j.

This file represents that subgroup over an arbitrary commutative base ring. The defining ideal is generated by Xᵢⱼ - δᵢⱼ for w i ≤ w j. Its Hopf-ideal closure is checked directly: the relations are stable under matrix multiplication, the identity matrix satisfies them, and the inverse of a block-unitriangular matrix is block unitriangular.

Main declarations

• TauCeti.GeneralLinear.weightUnipotentDefiningHopfIdeal: the Hopf ideal generated by the block-unitriangular relations.
• TauCeti.GeneralLinear.weightUnipotentGroupScheme: the resulting finite-type closed subgroup scheme of GL_N.
• TauCeti.GeneralLinear.mem_weightUnipotentDefiningPointsSubgroup_iff: its algebra-valued points are the block-triangular matrices acting trivially 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 advances the dynamic-unipotent route in Layer 7, "Structure theory", of the ReductiveGroups roadmap by constructing the scheme-level unipotent subgroup attached to a weight cocharacter.

def TauCeti.GeneralLinear.weightUnipotentRelationSet (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Set ↑(coordinateHopfAlgebra R N)

The matrix-coordinate relations saying that entries on and above the weight-block diagonal agree with the identity matrix.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.mem_weightUnipotentRelationSet_iff (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (x : ↑(coordinateHopfAlgebra R N)) : x ∈ weightUnipotentRelationSet R w ↔ ∃ (i : Fin N) (j : Fin N), w i ≤ w j ∧ x = genericMatrix R N i j - 1 i j

Membership in the weight-unipotent relation set means being a block-unitriangular matrix relation.

theorem TauCeti.GeneralLinear.sub_one_apply_mem_weightUnipotentRelationSet (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≤ w j) : genericMatrix R N i j - 1 i j ∈ weightUnipotentRelationSet R w

A block-unitriangular coordinate relation belongs to the defining relation set.

theorem TauCeti.GeneralLinear.quotient_genericMatrix_apply_of_le (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≤ w j) : (Ideal.Quotient.mkₐ R (Ideal.span (weightUnipotentRelationSet R w))) (genericMatrix R N i j) = 1 i j

A matrix coordinate on or above the weight-block diagonal is fixed in the quotient by the explicit weight-unipotent relation ideal.

noncomputable def TauCeti.GeneralLinear.weightUnipotentDefiningHopfIdeal (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : HopfIdeal R ↑(coordinateHopfAlgebra R N)

The Hopf ideal cutting out matrices which are block triangular for w and act as the identity on each associated-graded weight space.

Equations

• TauCeti.GeneralLinear.weightUnipotentDefiningHopfIdeal R w = TauCeti.HopfIdeal.ofSpan (TauCeti.GeneralLinear.weightUnipotentRelationSet R w) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.GeneralLinear.weightUnipotentDefiningHopfIdeal_toIdeal (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : (weightUnipotentDefiningHopfIdeal R w).toIdeal = Ideal.span (weightUnipotentRelationSet R w)

The underlying ideal is generated by the block-unitriangular coordinate relations.

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.weightUnipotentCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : CommHopfAlgCat R

The coordinate Hopf algebra of the weight-unipotent subgroup attached to w.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.GeneralLinear.weightUnipotentGroupScheme (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The affine group scheme represented by the weight-unipotent coordinate Hopf algebra.

Equations

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

noncomputable def TauCeti.GeneralLinear.weightUnipotentInclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : weightUnipotentGroupScheme R w ⟶ groupScheme R N

The closed immersion from the weight-unipotent subgroup into the named general linear group scheme.

Equations

• TauCeti.GeneralLinear.weightUnipotentInclusion R w = TauCeti.GeneralLinear.hopfIdealInclusion R N (TauCeti.GeneralLinear.weightUnipotentDefiningHopfIdeal R w)

theorem TauCeti.GeneralLinear.weightUnipotentInclusion_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : weightUnipotentInclusion R w = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w)) (CategoryTheory.eqToIso ⋯).hom

The weight-unipotent inclusion is the quotient-spectrum inclusion followed by the named identification with GL_N.

instance TauCeti.GeneralLinear.isClosedImmersion_weightUnipotentInclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightUnipotentInclusion R w).hom.hom)

The weight-unipotent inclusion into GL_N is a closed immersion.

instance TauCeti.GeneralLinear.locallyOfFiniteType_weightUnipotentGroupScheme (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : AlgebraicGeometry.LocallyOfFiniteType (weightUnipotentGroupScheme R w).X.hom

The weight-unipotent group scheme is locally of finite type over the base.

@[simp]

theorem TauCeti.GeneralLinear.mem_weightUnipotentDefiningPointsSubgroup_iff (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type u_1} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w) ↧A ↔ ∀ (i j : Fin N), w i ≤ w j → ↑((pointsMulEquiv N) g) i j = 1 i j

The subgroup cut out by the weight-unipotent ideal consists exactly of matrices whose (i,j) entry agrees with the identity matrix whenever w i ≤ w j.