The kernel of the represented weight-parabolic limit

Let w : Fin N → ℤ. The dynamic limit from the weight parabolic P(w) to its Levi subgroup L(w) is already represented by a morphism of affine group schemes. This file identifies its scheme-theoretic kernel with the represented weight-unipotent subgroup U(w). Thus the pointwise identity

U(w)(A) = ker (P(w)(A) → L(w)(A))

holds at the level of defining Hopf ideals, not only after choosing a value algebra A.

Main declarations

• TauCeti.GeneralLinear.Dynamic.mem_weightUnipotentInParabolicPointsSubgroup_iff_limit_eq_one: a represented parabolic point belongs to the relative unipotent subgroup exactly when its represented dynamic limit is the identity.
• TauCeti.GeneralLinear.Dynamic.kernelHopfIdeal_weightParabolicLimitCoordinateMap: the kernel Hopf ideal of the represented limit is the relative weight-unipotent Hopf ideal.
• TauCeti.GeneralLinear.Dynamic.weightParabolicLimitKernelIso: the resulting canonical isomorphism from the scheme-theoretic kernel to the weight-unipotent group scheme.

References

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

This advances the dynamic Levi-decomposition milestone in Layer 7, "Structure theory", of the ReductiveGroups roadmap. The kernel identification is the normal-factor input for identifying the represented weight parabolic with the semidirect product of its weight-unipotent and weight-Levi subgroups.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_weightUnipotentInParabolicPointsSubgroup_iff_limit_eq_one (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w) A ↔ (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightParabolicLimitCoordinateMap R w)).app A)) g = 1

A represented weight-parabolic point lies in the relative weight-unipotent subgroup exactly when its represented dynamic limit is the identity of the weight-Levi point group.

theorem TauCeti.GeneralLinear.Dynamic.kernelHopfIdeal_weightParabolicLimitCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : CommHopfAlgCat.kernelHopfIdeal (weightParabolicLimitCoordinateMap R w) = weightUnipotentInParabolicHopfIdeal R w

The scheme-theoretic kernel of the represented weight-parabolic limit is the represented weight-unipotent subgroup, as an equality of Hopf ideals in the parabolic coordinate algebra.

noncomputable def TauCeti.GeneralLinear.Dynamic.weightParabolicLimitKernelIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : CommHopfAlgCat.kernelSpec (weightParabolicLimitCoordinateMap R w) ≅ weightUnipotentGroupScheme R w

The scheme-theoretic kernel of the weight-parabolic limit is canonically the represented weight-unipotent group scheme.

Equations

• TauCeti.GeneralLinear.Dynamic.weightParabolicLimitKernelIso R w = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicGroupSchemeIso R w

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.weightParabolicLimitKernelIso_hom_comp_weightUnipotentToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : CategoryTheory.CategoryStruct.comp (weightParabolicLimitKernelIso R w).hom (weightUnipotentToParabolic R w) = CommHopfAlgCat.kernelSpecι (weightParabolicLimitCoordinateMap R w)

Under the kernel identification, the canonical kernel inclusion is the represented weight-unipotent inclusion into the weight parabolic.