Dynamic subgroup functors

The dynamic parabolic, Levi, and unipotent subgroups attached to a cocharacter are defined on points in TauCeti.Algebra.AlgebraicGroup.Dynamic.Parabolic. Their change-of-value-algebra theorems make these families into group-valued functors. This file packages those functors and their natural inclusions into the ambient functor of points.

The packaging is the interface needed to state representability. In particular, a dynamic subgroup is represented by an affine group scheme precisely when its functor below is naturally isomorphic to the functor of points of a commutative Hopf algebra.

Main declarations

• TauCeti.Cocharacter.parabolicFunctor: the dynamic parabolic as a group-valued functor.
• TauCeti.Cocharacter.leviFunctor: the dynamic Levi as a group-valued functor.
• TauCeti.Cocharacter.unipotentFunctor: the dynamic unipotent subgroup as a group-valued functor.
• TauCeti.Cocharacter.parabolicFunctorIncl, leviFunctorIncl, and unipotentFunctorIncl: their natural inclusions into the ambient functor of points.

References

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

This is the functorial interface for the dynamic approach to parabolic, Levi, and unipotent subgroups in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

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

Change of value algebra, restricted to a dynamic parabolic subgroup.

Equations

• TauCeti.Cocharacter.mapParabolic l φ = ((TauCeti.AlgHom.mapValue (CommAlgCat.Hom.hom φ)).domRestrict (TauCeti.Cocharacter.parabolic (↑A) l)).codRestrict (TauCeti.Cocharacter.parabolic (↑B) l) ⋯

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

Change of value algebra, restricted to a dynamic Levi subgroup.

Equations

• TauCeti.Cocharacter.mapLevi l φ = ((TauCeti.AlgHom.mapValue (CommAlgCat.Hom.hom φ)).domRestrict (TauCeti.Cocharacter.levi (↑A) l)).codRestrict (TauCeti.Cocharacter.levi (↑B) l) ⋯

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

Change of value algebra, restricted to a dynamic unipotent subgroup.

Equations

• TauCeti.Cocharacter.mapUnipotent l φ = ((TauCeti.AlgHom.mapValue (CommAlgCat.Hom.hom φ)).domRestrict (TauCeti.Cocharacter.unipotent (↑A) l)).codRestrict (TauCeti.Cocharacter.unipotent (↑B) l) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

The dynamic parabolic attached to a cocharacter, as a group-valued functor.

Equations

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

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

The dynamic Levi attached to a cocharacter, as a group-valued functor.

Equations

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

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

The dynamic unipotent subgroup attached to a cocharacter, as a group-valued functor.

Equations

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

theorem TauCeti.Cocharacter.parabolicFunctor_obj {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : (parabolicFunctor l).obj A = ↧↥(parabolic (↑A) l)

theorem TauCeti.Cocharacter.leviFunctor_obj {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : (leviFunctor l).obj A = ↧↥(levi (↑A) l)

theorem TauCeti.Cocharacter.unipotentFunctor_obj {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (A : CommAlgCat R) : (unipotentFunctor l).obj A = ↧↥(unipotent (↑A) l)

@[simp]

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

@[simp]

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

@[simp]

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

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

The dynamic parabolic functor includes naturally into the ambient functor of points.

Equations

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

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

The dynamic Levi functor includes naturally into the ambient functor of points.

Equations

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

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

The dynamic unipotent functor includes naturally into the ambient functor of points.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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