Geometry of general-linear weight Levis

For a weight w : Fin N → ℤ, the weight Levi in GL_N consists of the invertible matrices whose entries between distinct weight spaces vanish. Its coordinate algebra is the localization at the determinant of the polynomial algebra on the entries within equal-weight blocks.

This file constructs that presentation directly. The generic block-diagonal matrix supplies the map from the determinant localization defining GL_N; conversely, its surviving entries in the weight-Levi quotient supply the inverse map. The presentation proves smoothness over an arbitrary commutative base ring. Over a field it remains a domain after every scalar extension, and hence the weight Levi is geometrically connected.

Main declarations

• TauCeti.GeneralLinear.WeightLeviIndex: the matrix entries within equal-weight blocks.
• TauCeti.GeneralLinear.weightLeviCoordinateAlgEquiv: the localized polynomial presentation.
• TauCeti.GeneralLinear.instSmoothWeightLeviCoordinateHopfAlgebra: every weight Levi is smooth.
• TauCeti.GeneralLinear.geometricallyConnectedCommHopfAlgProperty_weightLeviCoordinateHopfAlgebra: every weight Levi over a field is geometrically connected.

References

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

The quotient/evaluation equivalence and its inverse-map proofs, together with the smoothness, domain, and geometric-connectedness arguments, are adapted from the construction in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Weight.Unipotent.Geometry.

@[reducible, inline]

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

Pairs indexing matrix entries within one weight space.

Equations

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

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

The generic matrix whose free entries are those within equal-weight blocks.

Equations

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

@[simp]

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

An entry within one weight block is its corresponding polynomial variable.

@[simp]

theorem TauCeti.GeneralLinear.weightLeviPolynomialGenericMatrix_apply_of_ne (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≠ w j) : weightLeviPolynomialGenericMatrix R w i j = 0

An entry between distinct weight blocks vanishes.

@[reducible, inline]

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

The localized polynomial presentation of a weight Levi.

Equations

• TauCeti.GeneralLinear.WeightLeviCoordinateRing R w = Localization.Away (TauCeti.GeneralLinear.weightLeviPolynomialGenericMatrix R w).det

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

The generic weight-Levi matrix in its localized coordinate ring.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightLeviLocalizedGenericMatrix_apply_of_eq (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i = w j) : weightLeviLocalizedGenericMatrix R w i j = (IsScalarTower.toAlgHom R (MvPolynomial (WeightLeviIndex w) R) (WeightLeviCoordinateRing R w)) (MvPolynomial.X ⟨(i, j), hij⟩)

A localized generic entry within one weight block is the corresponding localized variable.

@[simp]

theorem TauCeti.GeneralLinear.weightLeviLocalizedGenericMatrix_apply_of_ne (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≠ w j) : weightLeviLocalizedGenericMatrix R w i j = 0

A localized generic entry between distinct weight blocks vanishes.

theorem TauCeti.GeneralLinear.isUnit_det_weightLeviLocalizedGenericMatrix (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : IsUnit (weightLeviLocalizedGenericMatrix R w).det

The determinant of the localized generic weight-Levi matrix is a unit.

@[simp]

theorem TauCeti.GeneralLinear.weightLeviQuotient_mk_genericMatrix_apply_of_ne (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {i j : Fin N} (hij : w i ≠ w j) : (Ideal.Quotient.mk (weightLeviDefiningHopfIdeal R w).toIdeal) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))) = 0

In the weight-Levi quotient, an ambient entry between different weight blocks is zero.

noncomputable def TauCeti.GeneralLinear.weightLeviCoordinateAlgEquiv (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : ↑(weightLeviCoordinateHopfAlgebra R w) ≃ₐ[R] WeightLeviCoordinateRing R w

The weight-Levi coordinate algebra is the determinant localization of the polynomial algebra on entries lying within equal-weight blocks.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightLeviCoordinateAlgEquiv_mk_genericMatrix_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (i j : Fin N) : (weightLeviCoordinateAlgEquiv R w) ((Ideal.Quotient.mk (weightLeviDefiningHopfIdeal R w).toIdeal) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j))))) = weightLeviLocalizedGenericMatrix R w i j

The localized polynomial presentation sends a quotient matrix entry to the corresponding entry of the generic block-diagonal matrix.

@[simp]

theorem TauCeti.GeneralLinear.weightLeviCoordinateAlgEquiv_symm_algebraMap_X (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (ij : WeightLeviIndex w) : (weightLeviCoordinateAlgEquiv R w).symm ((algebraMap (MvPolynomial (WeightLeviIndex w) R) (WeightLeviCoordinateRing R w)) (MvPolynomial.X ij)) = (Ideal.Quotient.mkₐ R (weightLeviDefiningHopfIdeal R w).toIdeal) (genericMatrix R N (↑ij).1 (↑ij).2)

The inverse localized-polynomial presentation sends a block variable to its surviving quotient-matrix entry.

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

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

theorem TauCeti.GeneralLinear.weightLeviPolynomialGenericMatrix_det_ne_zero {N : ℕ} (R : Type u) [CommRing R] [Nontrivial R] (w : Fin N → ℤ) : (weightLeviPolynomialGenericMatrix R w).det ≠ 0

The determinant of the generic block-diagonal matrix is a nonzero polynomial over a nontrivial base ring.

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

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

noncomputable def TauCeti.GeneralLinear.weightLeviCoordinateRingBaseChangeAlgEquiv {N : ℕ} (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (w : Fin N → ℤ) : TensorProduct k K (WeightLeviCoordinateRing k w) ≃ₐ[K] WeightLeviCoordinateRing K w

Scalar extension of the localized polynomial presentation is the corresponding presentation over the extended base ring.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightLeviCoordinateRingBaseChangeAlgEquiv_tmul_algebraMap {N : ℕ} (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (w : Fin N → ℤ) (s : K) (p : MvPolynomial (WeightLeviIndex w) k) : (weightLeviCoordinateRingBaseChangeAlgEquiv k K w) (s ⊗ₜ[k] (algebraMap (MvPolynomial (WeightLeviIndex w) k) (WeightLeviCoordinateRing k w)) p) = s • (algebraMap (MvPolynomial (WeightLeviIndex w) K) (WeightLeviCoordinateRing K w)) ((MvPolynomial.map (algebraMap k K)) p)

Base change sends a scalar tensored with a localized polynomial coordinate to that scalar times the same polynomial with its coefficients extended to the new base.

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

The weight Levi is geometrically connected over every field.