Geometry of general-linear weight parabolics

Every weight Levi has a localized block-coordinate presentation that makes it smooth and geometrically connected. Combining these facts with the represented weight-parabolic Levi decomposition

U(w) ⋊ L(w) ≅ P(w)

shows that every weight parabolic is smooth over a commutative ring and geometrically connected over a field.

Main declarations

• TauCeti.GeneralLinear.smoothCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra: smoothness of a weight parabolic.
• TauCeti.GeneralLinear. geometricallyConnectedCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra: geometric connectedness of a weight parabolic.

References

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

theorem TauCeti.GeneralLinear.smoothCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra {N : ℕ} (R : Type u) [CommRing R] (w : Fin N → ℤ) : smoothCommHopfAlgProperty R (weightParabolicCoordinateHopfAlgebra R w)

The coordinate Hopf algebra of a weight parabolic is smooth over every commutative ring.

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

The coordinate Hopf algebra of a weight parabolic is geometrically connected over every field.