Geometry of injective-weight parabolics

An injective weight has diagonal split torus as its Levi factor. Combining this identification with the represented weight-parabolic Levi decomposition

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

shows that its weight parabolic is smooth and geometrically connected over every field.

Main declarations

• TauCeti.GeneralLinear.smoothCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra: smoothness of an injective-weight parabolic.
• TauCeti.GeneralLinear. geometricallyConnectedCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra: geometric connectedness of an injective-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.

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

theorem TauCeti.GeneralLinear.smoothCommHopfAlgProperty_weightParabolicCoordinateHopfAlgebra {N : ℕ} (k : Type u) [Field k] (w : Fin N → ℤ) (hw : Function.Injective w) : smoothCommHopfAlgProperty k (weightParabolicCoordinateHopfAlgebra k w)

The coordinate Hopf algebra of an injective-weight parabolic is smooth over every field.

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

The coordinate Hopf algebra of an injective-weight parabolic is geometrically connected over every field.