Naturality of the dynamic Levi decomposition

The dynamic Levi decomposition identifies the parabolic subgroup attached to a cocharacter with the semidirect product of its unipotent and Levi subgroups. This file proves that the identification commutes with extension of the commutative value algebra.

For a cocharacter l, extension along A ⟶ B preserves the conjugation action of Z(l) on U(l). Hence the maps on the two factors combine to a homomorphism between their semidirect products. These homomorphisms form a group-valued functor, and the pointwise Levi decompositions assemble into a natural isomorphism

U(l)(-) ⋊ Z(l)(-) ≅ P(l)(-).

This is the functorial bridge between the pointwise decomposition and the represented weight parabolic, Levi, and unipotent subgroups of GLₙ.

Main declarations

• TauCeti.Cocharacter.leviSemidirectMap: extension of the value algebra on the semidirect product.
• TauCeti.Cocharacter.leviSemidirectFunctor: the dynamic semidirect product as a group-valued functor.
• TauCeti.Cocharacter.limitToLeviNatTrans: the dynamic limit as a natural transformation from the parabolic functor to the Levi functor.
• TauCeti.Cocharacter.leviToParabolicNatTrans: the Levi inclusions as a natural transformation splitting the dynamic limit.
• TauCeti.Cocharacter.leviDecompositionNatIso: the dynamic Levi decomposition as a natural isomorphism of group-valued functors.

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.

@[simp]

theorem TauCeti.Cocharacter.mapLevi_limitToLevi {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↥(parabolic (↑A) l)) : (mapLevi l φ) ((limitToLevi (↑A) l) g) = (limitToLevi (↑B) l) ((mapParabolic l φ) g)

Extension of the value algebra commutes with the Levi-valued dynamic limit.

noncomputable def TauCeti.Cocharacter.limitToLeviNatTrans {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : parabolicFunctor l ⟶ leviFunctor l

The dynamic limit homomorphisms P(l)(A) → Z(l)(A) form a natural transformation in the commutative value algebra A.

Equations

• TauCeti.Cocharacter.limitToLeviNatTrans l = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.Cocharacter.limitToLevi (↑A) l), naturality := ⋯ }

@[simp]

theorem TauCeti.Cocharacter.limitToLeviNatTrans_app {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : (limitToLeviNatTrans l).app A = GrpCat.ofHom (limitToLevi (↑A) l)

The component of the dynamic limit natural transformation is the pointwise limit homomorphism.

@[simp]

theorem TauCeti.Cocharacter.mapParabolic_unipotentToParabolic {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↥(unipotent (↑A) l)) : (mapParabolic l φ) ((unipotentToParabolic (↑A) l) g) = (unipotentToParabolic (↑B) l) ((mapUnipotent l φ) g)

Extension of the value algebra commutes with inclusion of the dynamic unipotent subgroup into the dynamic parabolic.

@[simp]

theorem TauCeti.Cocharacter.mapParabolic_leviToParabolic {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↥(levi (↑A) l)) : (mapParabolic l φ) ((leviToParabolic (↑A) l) g) = (leviToParabolic (↑B) l) ((mapLevi l φ) g)

Extension of the value algebra commutes with inclusion of the dynamic Levi subgroup into the dynamic parabolic.

noncomputable def TauCeti.Cocharacter.leviToParabolicNatTrans {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : leviFunctor l ⟶ parabolicFunctor l

The inclusions Z(l)(A) → P(l)(A) form a natural transformation in the commutative value algebra A.

Equations

• TauCeti.Cocharacter.leviToParabolicNatTrans l = { app := fun (A : CommAlgCat R) => GrpCat.ofHom (TauCeti.Cocharacter.leviToParabolic (↑A) l), naturality := ⋯ }

@[simp]

theorem TauCeti.Cocharacter.leviToParabolicNatTrans_app {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : (leviToParabolicNatTrans l).app A = GrpCat.ofHom (leviToParabolic (↑A) l)

The component of the natural Levi inclusion is the pointwise subgroup inclusion.

@[simp]

theorem TauCeti.Cocharacter.leviToParabolicNatTrans_comp_limitToLeviNatTrans {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : CategoryTheory.CategoryStruct.comp (leviToParabolicNatTrans l) (limitToLeviNatTrans l) = CategoryTheory.CategoryStruct.id (leviFunctor l)

The natural Levi inclusion is a section of the dynamic limit.

@[simp]

theorem TauCeti.Cocharacter.mapUnipotent_leviConjugation {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (z : ↥(levi (↑A) l)) (g : ↥(unipotent (↑A) l)) : (mapUnipotent l φ) (((leviConjugation (↑A) l) z) g) = ((leviConjugation (↑B) l) ((mapLevi l φ) z)) ((mapUnipotent l φ) g)

Extension of the value algebra preserves the conjugation action of the dynamic Levi subgroup on the dynamic unipotent subgroup.

noncomputable def TauCeti.Cocharacter.leviSemidirectMap {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) : ↥(unipotent (↑A) l) ⋊[leviConjugation (↑A) l] ↥(levi (↑A) l) →* ↥(unipotent (↑B) l) ⋊[leviConjugation (↑B) l] ↥(levi (↑B) l)

Extension of the value algebra on the semidirect product in the dynamic Levi decomposition.

Equations

• TauCeti.Cocharacter.leviSemidirectMap l φ = SemidirectProduct.map (TauCeti.Cocharacter.mapUnipotent l φ) (TauCeti.Cocharacter.mapLevi l φ) ⋯

@[simp]

theorem TauCeti.Cocharacter.leviSemidirectMap_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↥(unipotent (↑A) l) ⋊[leviConjugation (↑A) l] ↥(levi (↑A) l)) : (leviSemidirectMap l φ) g = ⟨(mapUnipotent l φ) g.left, (mapLevi l φ) g.right⟩

Extension on the dynamic Levi semidirect product acts coordinatewise.

theorem TauCeti.Cocharacter.mapParabolic_leviDecompositionMulEquiv_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) (g : ↥(unipotent (↑A) l) ⋊[leviConjugation (↑A) l] ↥(levi (↑A) l)) : (mapParabolic l φ) ((leviDecompositionMulEquiv (↑A) l) g) = (leviDecompositionMulEquiv (↑B) l) ((leviSemidirectMap l φ) g)

Extension of the value algebra commutes with the dynamic Levi decomposition equivalence.

noncomputable def TauCeti.Cocharacter.leviSemidirectFunctor {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : CategoryTheory.Functor (CommAlgCat R) GrpCat

The semidirect product U(l)(A) ⋊ Z(l)(A) in the dynamic Levi decomposition, functorial in the commutative value algebra A.

Equations

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

@[simp]

theorem TauCeti.Cocharacter.leviSemidirectFunctor_map {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) {A B : CommAlgCat R} (φ : A ⟶ B) : (leviSemidirectFunctor l).map φ = GrpCat.ofHom (leviSemidirectMap l φ)

The dynamic Levi semidirect-product functor maps a homomorphism by extension on its unipotent and Levi coordinates.

noncomputable def TauCeti.Cocharacter.leviDecompositionNatIso {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) : leviSemidirectFunctor l ≅ parabolicFunctor l

The functorial dynamic Levi decomposition. The semidirect product of the dynamic unipotent and Levi subgroup functors is naturally isomorphic to the dynamic parabolic functor.

Equations

• TauCeti.Cocharacter.leviDecompositionNatIso l = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat R) => (TauCeti.Cocharacter.leviDecompositionMulEquiv (↑A) l).toGrpIso) ⋯

@[simp]

theorem TauCeti.Cocharacter.leviDecompositionNatIso_hom_app_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (g : ↥(unipotent (↑A) l) ⋊[leviConjugation (↑A) l] ↥(levi (↑A) l)) : (CategoryTheory.ConcreteCategory.hom ((leviDecompositionNatIso l).hom.app A)) g = (leviDecompositionMulEquiv (↑A) l) g

The forward component of the functorial dynamic Levi decomposition is the pointwise semidirect-product equivalence.

@[simp]

theorem TauCeti.Cocharacter.leviDecompositionNatIso_inv_app_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) (g : ↥(parabolic (↑A) l)) : (CategoryTheory.ConcreteCategory.hom ((leviDecompositionNatIso l).inv.app A)) g = (leviDecompositionMulEquiv (↑A) l).symm g

The inverse component of the functorial dynamic Levi decomposition is the inverse pointwise semidirect-product equivalence.