The dynamic Levi decomposition as a semidirect product

Let l : 𝔾ₘ → G be a cocharacter of an affine group. The dynamic parabolic P(l) has a limit homomorphism onto its Levi subgroup Z(l), whose kernel is the dynamic unipotent subgroup U(l). The inclusion of Z(l) in P(l) splits this homomorphism.

This file packages those facts as a split group extension and applies Mathlib's general theorem for split extensions. For every commutative value algebra A this gives the canonical semidirect-product equivalence

U(l)(A) ⋊ Z(l)(A) ≃* P(l)(A).

The action is conjugation through the two subgroup inclusions. Characteristic lemmas identify the equivalence with multiplication, its Levi coordinate with the limit, and its unipotent coordinate with g · limit(g)⁻¹. Thus downstream representability arguments can use the bundled equivalence without reopening the existence-and-uniqueness proof of the pointwise Levi factorization.

Main declarations

• TauCeti.Cocharacter.limitToLevi: the limit homomorphism with codomain restricted to the Levi subgroup.
• TauCeti.Cocharacter.leviGroupExtension: the exact sequence 1 → U(l)(A) → P(l)(A) → Z(l)(A) → 1.
• TauCeti.Cocharacter.leviGroupExtensionSplitting: its canonical splitting.
• TauCeti.Cocharacter.leviConjugation: the resulting action of Z(l)(A) on U(l)(A).
• TauCeti.Cocharacter.leviDecompositionMulEquiv: the dynamic Levi decomposition as a multiplicative equivalence.

References

• G. R. Kempf, Instability in invariant theory, Annals of Mathematics 108 (1978), §2.
• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.
• J. S. Milne, Algebraic Groups (2017), Chapter 13.

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

noncomputable def TauCeti.Cocharacter.limitToLevi {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : ↥(parabolic A l) →* ↥(levi A l)

The dynamic limit homomorphism, with its codomain restricted to the Levi subgroup.

Equations

• TauCeti.Cocharacter.limitToLevi A l = (TauCeti.Cocharacter.limit A l).codRestrict (TauCeti.Cocharacter.levi A l) ⋯

@[simp]

theorem TauCeti.Cocharacter.coe_limitToLevi_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(parabolic A l)) : ↑((limitToLevi A l) g) = (limit A l) g

The Levi-valued limit has the same underlying point as the ambient-valued limit.

noncomputable def TauCeti.Cocharacter.unipotentToParabolic {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : ↥(unipotent A l) →* ↥(parabolic A l)

Inclusion of the dynamic unipotent subgroup into the dynamic parabolic.

Equations

• TauCeti.Cocharacter.unipotentToParabolic A l = Subgroup.inclusion ⋯

noncomputable def TauCeti.Cocharacter.leviToParabolic {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : ↥(levi A l) →* ↥(parabolic A l)

Inclusion of the dynamic Levi subgroup into the dynamic parabolic.

Equations

• TauCeti.Cocharacter.leviToParabolic A l = Subgroup.inclusion ⋯

@[simp]

theorem TauCeti.Cocharacter.coe_unipotentToParabolic_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(unipotent A l)) : ↑((unipotentToParabolic A l) g) = ↑g

The unipotent inclusion does not change the underlying point.

@[simp]

theorem TauCeti.Cocharacter.coe_leviToParabolic_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(levi A l)) : ↑((leviToParabolic A l) g) = ↑g

The Levi inclusion does not change the underlying point.

theorem TauCeti.Cocharacter.range_unipotentToParabolic_eq_ker_limitToLevi {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : (unipotentToParabolic A l).range = (limitToLevi A l).ker

The dynamic unipotent subgroup is exactly the kernel of the Levi-valued limit, as a subgroup of the dynamic parabolic.

theorem TauCeti.Cocharacter.limitToLevi_surjective {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : Function.Surjective ⇑(limitToLevi A l)

The Levi-valued limit is surjective; the Levi inclusion supplies a preimage of every element.

noncomputable def TauCeti.Cocharacter.leviGroupExtension {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : GroupExtension ↥(unipotent A l) ↥(parabolic A l) ↥(levi A l)

The dynamic parabolic is an extension of its Levi subgroup by its dynamic unipotent subgroup.

Equations

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

@[simp]

theorem TauCeti.Cocharacter.leviGroupExtension_inl_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (u : ↥(unipotent A l)) : (leviGroupExtension A l).inl u = (unipotentToParabolic A l) u

The kernel inclusion of the dynamic Levi group extension is the subgroup inclusion.

@[simp]

theorem TauCeti.Cocharacter.leviGroupExtension_rightHom_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(parabolic A l)) : (leviGroupExtension A l).rightHom g = (limitToLevi A l) g

The projection of the dynamic Levi group extension is the Levi-valued limit.

noncomputable def TauCeti.Cocharacter.leviGroupExtensionSplitting {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : (leviGroupExtension A l).Splitting

The Levi inclusion canonically splits the dynamic Levi group extension.

Equations

• TauCeti.Cocharacter.leviGroupExtensionSplitting A l = { toMonoidHom := TauCeti.Cocharacter.leviToParabolic A l, rightInverse_rightHom := ⋯ }

@[simp]

theorem TauCeti.Cocharacter.leviGroupExtensionSplitting_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (z : ↥(levi A l)) : (leviGroupExtensionSplitting A l) z = (leviToParabolic A l) z

The canonical splitting of the dynamic Levi extension is the Levi subgroup inclusion.

@[simp]

theorem TauCeti.Cocharacter.limitToLevi_leviToParabolic {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (z : ↥(levi A l)) : (limitToLevi A l) ((leviToParabolic A l) z) = z

The dynamic limit retracts the inclusion of the Levi subgroup into the parabolic subgroup.

noncomputable def TauCeti.Cocharacter.leviConjugation {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : ↥(levi A l) →* MulAut ↥(unipotent A l)

The action of the dynamic Levi subgroup on the dynamic unipotent subgroup by conjugation.

Equations

• TauCeti.Cocharacter.leviConjugation A l = (TauCeti.Cocharacter.leviGroupExtensionSplitting A l).conjAct

theorem TauCeti.Cocharacter.leviConjugation_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (z : ↥(levi A l)) (u : ↥(unipotent A l)) : ((leviConjugation A l) z) u = ((leviGroupExtension A l).conjAct ((leviToParabolic A l) z)) u

The Levi action is the conjugation action associated to the dynamic Levi group extension.

@[simp]

theorem TauCeti.Cocharacter.coe_leviConjugation_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (z : ↥(levi A l)) (u : ↥(unipotent A l)) : ↑(((leviConjugation A l) z) u) = ↑z * ↑u * ↑z⁻¹

The Levi action is ordinary conjugation on the underlying ambient points.

noncomputable def TauCeti.Cocharacter.leviDecompositionMulEquiv {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) : ↥(unipotent A l) ⋊[leviConjugation A l] ↥(levi A l) ≃* ↥(parabolic A l)

The dynamic Levi decomposition. The semidirect product of the dynamic unipotent and Levi subgroups is canonically equivalent to the dynamic parabolic.

Equations

• TauCeti.Cocharacter.leviDecompositionMulEquiv A l = (TauCeti.Cocharacter.leviGroupExtensionSplitting A l).semidirectProductMulEquiv

@[simp]

theorem TauCeti.Cocharacter.leviDecompositionMulEquiv_apply {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (x : ↥(unipotent A l) ⋊[leviConjugation A l] ↥(levi A l)) : (leviDecompositionMulEquiv A l) x = (unipotentToParabolic A l) x.left * (leviToParabolic A l) x.right

The dynamic Levi decomposition equivalence sends (u, z) to the product of the two subgroup inclusions.

@[simp]

theorem TauCeti.Cocharacter.leviDecompositionMulEquiv_symm_apply_right {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(parabolic A l)) : ((leviDecompositionMulEquiv A l).symm g).right = (limitToLevi A l) g

The Levi coordinate of the inverse decomposition is the limit of the parabolic point.

@[simp]

theorem TauCeti.Cocharacter.coe_leviDecompositionMulEquiv_symm_apply_left {R : Type u} {H : Type v} (A : Type w) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H →ₐc[R] LaurentPolynomial R) (g : ↥(parabolic A l)) : ↑((leviDecompositionMulEquiv A l).symm g).left = ↑g * ((limit A l) g)⁻¹

The unipotent coordinate of the inverse decomposition is g * limit(g)⁻¹.