Injective-weight Levis and the diagonal torus

For a weight w : Fin N → ℤ, the weight Levi consists of the invertible matrices whose (i,j) entry vanishes when w i ≠ w j. If w is injective, these are precisely the diagonal matrices. This file identifies the corresponding coordinate Hopf algebra with that of the diagonal split torus.

Main declarations

• TauCeti.GeneralLinear.weightLeviDiagonalCoordinateIso: the coordinate Hopf algebra of an injective-weight Levi is that of the diagonal split torus.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 12--13.
• T. A. Springer, Linear Algebraic Groups, Sections 6.2--6.3.

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

noncomputable def TauCeti.GeneralLinear.weightLeviDiagonalCoordinateIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (hw : Function.Injective w) : weightLeviCoordinateHopfAlgebra R w ≅ ↧(MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ)))

The coordinate Hopf algebra of an injective-weight Levi is the coordinate ring of the diagonal split torus.

Equations

• TauCeti.GeneralLinear.weightLeviDiagonalCoordinateIso R w hw = CategoryTheory.asIso (TauCeti.GeneralLinear.weightLeviDiagonalCoordinateMap✝ R w)

@[simp]

theorem TauCeti.GeneralLinear.weightLeviCoordinateMap_comp_weightLeviDiagonalCoordinateIso_hom (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (hw : Function.Injective w) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w)) (weightLeviDiagonalCoordinateIso R w hw).hom = diagonalTorusCoordinateMap

The injective-weight Levi coordinate isomorphism restricts the ambient general-linear coordinate map to the diagonal-torus coordinate map.