Representability of the dynamic subgroups of GL₂

For the cocharacter t ↦ diag(t, 1), the dynamic parabolic, Levi, and unipotent subgroup functors are represented by the standard upper-triangular Borel, diagonal torus, and positive root subgroup. This upgrades the pointwise calculations in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.GL2.Subgroups to natural isomorphisms of group-valued functors.

Concretely, the three representing coordinate Hopf algebras are

• Borel.coordinateHopfAlgebra R for the dynamic parabolic;
• the rank-two split-torus group algebra for the dynamic Levi;
• AdditiveGroup.coordinateHopfAlgebra R for the dynamic unipotent subgroup.

The natural isomorphisms commute with the inclusions into GL₂: on every value algebra their components are the existing Borel point equivalence, diagonal-torus point map, and positive root-subgroup point map.

Main declarations

• TauCeti.GeneralLinear.Dynamic.GL2.borelPointsIsoParabolicFunctor represents the dynamic parabolic functor by the Borel coordinate Hopf algebra.
• TauCeti.GeneralLinear.Dynamic.GL2.splitTorusPointsIsoLeviFunctor represents the dynamic Levi functor by the rank-two split torus.
• TauCeti.GeneralLinear.Dynamic.GL2.additivePointsIsoUnipotentFunctor represents the dynamic unipotent functor by the additive group.

References

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

This supplies scheme-level representability for the rank-one dynamic-parabolic route in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.borelPointsIsoParabolicFunctor {R : Type u} [CommRing R] : HopfAlgebra.pointsFunctor ≅ Cocharacter.parabolicFunctor dynamicCocharacter

The Borel coordinate Hopf algebra represents the dynamic parabolic functor for t ↦ diag(t, 1).

Equations

• TauCeti.GeneralLinear.Dynamic.GL2.borelPointsIsoParabolicFunctor = ⋯.mpr (TauCeti.GeneralLinear.Dynamic.weightParabolicPointsIso R TauCeti.GeneralLinear.Borel.weights)

The dynamic Levi

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.splitTorusToLevi {R : Type u} [CommRing R] (A : CommAlgCat R) : ↑(HopfAlgebra.points A) →* ↥(Cocharacter.levi (↑A) dynamicCocharacter)

The diagonal-torus point map, with codomain restricted to the dynamic Levi.

Equations

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

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.splitTorusLeviMulEquiv {R : Type u} [CommRing R] (A : CommAlgCat R) : ↑(HopfAlgebra.points A) ≃* ↥(Cocharacter.levi (↑A) dynamicCocharacter)

The pointwise equivalence from the rank-two split torus to the dynamic Levi.

Equations

• TauCeti.GeneralLinear.Dynamic.GL2.splitTorusLeviMulEquiv A = MulEquiv.ofBijective (TauCeti.GeneralLinear.Dynamic.GL2.splitTorusToLevi A) ⋯

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.coe_splitTorusLeviMulEquiv_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ↑((splitTorusLeviMulEquiv A) f) = diagonalTorusPoints f

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.splitTorusPointsIsoLeviFunctor {R : Type u} [CommRing R] : HopfAlgebra.pointsFunctor ≅ Cocharacter.leviFunctor dynamicCocharacter

The rank-two split-torus coordinate Hopf algebra represents the dynamic Levi functor for t ↦ diag(t, 1).

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.splitTorusPointsIsoLeviFunctor_hom_app_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (splitTorusPointsIsoLeviFunctor.hom.app A)) f = (splitTorusLeviMulEquiv A) f

The forward component of splitTorusPointsIsoLeviFunctor is the pointwise split-torus equivalence.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.splitTorusPointsIsoLeviFunctor_inv_app_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (g : ↥(Cocharacter.levi (↑A) dynamicCocharacter)) : (CategoryTheory.ConcreteCategory.hom (splitTorusPointsIsoLeviFunctor.inv.app A)) g = (splitTorusLeviMulEquiv A).symm g

The inverse component of splitTorusPointsIsoLeviFunctor is the inverse pointwise split-torus equivalence.

The dynamic unipotent subgroup

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.additiveToUnipotent {R : Type u} [CommRing R] (A : CommAlgCat R) : ↑(HopfAlgebra.points A) →* ↥(Cocharacter.unipotent (↑A) dynamicCocharacter)

The positive root-subgroup point map, with codomain restricted to the dynamic unipotent subgroup.

Equations

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

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.additiveUnipotentMulEquiv {R : Type u} [CommRing R] (A : CommAlgCat R) : ↑(HopfAlgebra.points A) ≃* ↥(Cocharacter.unipotent (↑A) dynamicCocharacter)

The pointwise equivalence from the additive group to the dynamic unipotent subgroup.

Equations

• TauCeti.GeneralLinear.Dynamic.GL2.additiveUnipotentMulEquiv A = MulEquiv.ofBijective (TauCeti.GeneralLinear.Dynamic.GL2.additiveToUnipotent A) ⋯

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.coe_additiveUnipotentMulEquiv_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ↑((additiveUnipotentMulEquiv A) f) = (rootSubgroupPoints coe_additiveUnipotentMulEquiv_apply._proof_1) f

noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.additivePointsIsoUnipotentFunctor {R : Type u} [CommRing R] : HopfAlgebra.pointsFunctor ≅ Cocharacter.unipotentFunctor dynamicCocharacter

The additive-group coordinate Hopf algebra represents the dynamic unipotent functor for t ↦ diag(t, 1).

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.additivePointsIsoUnipotentFunctor_hom_app_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (additivePointsIsoUnipotentFunctor.hom.app A)) f = (additiveUnipotentMulEquiv A) f

The forward component of additivePointsIsoUnipotentFunctor is the pointwise additive equivalence.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.GL2.additivePointsIsoUnipotentFunctor_inv_app_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (g : ↥(Cocharacter.unipotent (↑A) dynamicCocharacter)) : (CategoryTheory.ConcreteCategory.hom (additivePointsIsoUnipotentFunctor.inv.app A)) g = (additiveUnipotentMulEquiv A).symm g

The inverse component of additivePointsIsoUnipotentFunctor is the inverse pointwise additive equivalence.