Weight-parabolic subgroup schemes of the general linear group

An integer weight w i on each coordinate of GL_N cuts out the matrices whose (i,j) entry vanishes whenever w i < w j. This file represents that weight parabolic by a finite-type closed subgroup scheme over an arbitrary commutative base ring.

The defining Hopf ideal is generated by the forbidden matrix coordinates X_ij with w i < w j. Comultiplication preserves this ideal because, for every intermediate index k, either w i < w k or w k < w j. Antipode stability follows because the inverse of a block-triangular invertible matrix is block triangular.

Main declarations

• TauCeti.GeneralLinear.weightParabolicDefiningHopfIdeal: the Hopf ideal generated by the forbidden coordinates.
• TauCeti.GeneralLinear.weightParabolicGroupScheme: the resulting closed subgroup scheme.
• TauCeti.GeneralLinear.weightParabolicInclusion: its closed immersion into GL_N.

References

• G. R. Kempf, Instability in invariant theory, Annals of Mathematics 108 (1978), §2.
• J. S. Milne, Algebraic Groups (2017), Chapter 13.
• The Hopf-ideal quotient, closed-subgroup packaging, and algebra-valued points construction adapt TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Borel (which in turn adapts TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Basic).

This advances the dynamic-parabolic route in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

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

The set of matrix coordinates forbidden by the decreasing weight filtration.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.mem_weightParabolicRelationSet_iff (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (x : ↑(coordinateHopfAlgebra R N)) : x ∈ weightParabolicRelationSet R w ↔ ∃ (i : Fin N) (j : Fin N), w i < w j ∧ x = (coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))

Membership in the weight-parabolic relation set means being a forbidden matrix coordinate.

theorem TauCeti.GeneralLinear.X_mem_weightParabolicRelationSet (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i < w j) : (coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j))) ∈ weightParabolicRelationSet R w

A forbidden matrix coordinate belongs to the weight-parabolic relation set.

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

The Hopf ideal cutting out matrices block triangular for the decreasing weight filtration.

Equations

• TauCeti.GeneralLinear.weightParabolicDefiningHopfIdeal R w = TauCeti.HopfIdeal.ofSpan (TauCeti.GeneralLinear.weightParabolicRelationSet R w) ⋯ ⋯ ⋯

@[simp]

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

The underlying ideal is generated by precisely the forbidden matrix coordinates.

@[reducible, inline]

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

The coordinate Hopf algebra of the weight parabolic attached to w.

Equations

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

noncomputable def TauCeti.GeneralLinear.weightParabolicCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : coordinateHopfAlgebra R N ⟶ weightParabolicCoordinateHopfAlgebra R w

The quotient coordinate morphism from O(GL_N) to the weight-parabolic coordinate algebra.

Equations

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

theorem TauCeti.GeneralLinear.weightParabolicCoordinateMap_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (h : ↑(coordinateHopfAlgebra R N)) : (CommHopfAlgCat.Hom.hom (weightParabolicCoordinateMap R w)) h = (Ideal.Quotient.mkₐ R (weightParabolicDefiningHopfIdeal R w).toIdeal) h

The weight-parabolic coordinate morphism sends an ambient coordinate to its quotient class.

theorem TauCeti.GeneralLinear.weightParabolicCoordinateMap_surjective (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (weightParabolicCoordinateMap R w))

The quotient coordinate morphism defining the weight parabolic is surjective.

@[simp]

theorem TauCeti.GeneralLinear.weightParabolicCoordinateMap_X (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i < w j) : (CommHopfAlgCat.Hom.hom (weightParabolicCoordinateMap R w)) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))) = 0

A forbidden coordinate vanishes in the weight-parabolic coordinate algebra.

@[reducible, inline]

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

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

Equations

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

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

The closed immersion from the weight parabolic into the named general linear group scheme.

Equations

• TauCeti.GeneralLinear.weightParabolicInclusion R w = TauCeti.GeneralLinear.hopfIdealInclusion R N (TauCeti.GeneralLinear.weightParabolicDefiningHopfIdeal R w)

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

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

@[simp]

theorem TauCeti.GeneralLinear.weightParabolicInclusion_coordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage (CategoryTheory.CategoryStruct.comp (weightParabolicInclusion R w) (CategoryTheory.eqToHom ⋯))).unop = weightParabolicCoordinateMap R w

The coordinate morphism recovered from the weight-parabolic inclusion is the quotient coordinate map.

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

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

noncomputable def TauCeti.GeneralLinear.weightParabolicFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : FiniteTypeCommHopfAlgCat R

The weight-parabolic coordinate Hopf algebra with its finite-type property.

Equations

• TauCeti.GeneralLinear.weightParabolicFiniteTypeCoordinateHopfAlgebra R w = { obj := TauCeti.GeneralLinear.weightParabolicCoordinateHopfAlgebra R w, property := ⋯ }

@[simp]

theorem TauCeti.GeneralLinear.weightParabolicFiniteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : (weightParabolicFiniteTypeCoordinateHopfAlgebra R w).obj = weightParabolicCoordinateHopfAlgebra R w

The finite-type package has the weight-parabolic coordinate Hopf algebra as its object.

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

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

@[simp]

theorem TauCeti.GeneralLinear.mem_weightParabolicDefiningPointsSubgroup_iff_blockTriangular (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) (weightParabolicDefiningHopfIdeal R w) ↧A ↔ (↑((pointsMulEquiv N) g)).BlockTriangular (⇑OrderDual.toDual ∘ w)

The subgroup cut out by the weight-parabolic ideal consists exactly of block-triangular ambient points.