The dynamic Levi and unipotent subgroups of GL₂

For the cocharacter t ↦ diag(t, 1) of GL₂, the dynamic parabolic is the upper-triangular Borel subgroup. This file identifies the other two pieces of its dynamic Levi decomposition:

• the dynamic Levi subgroup is the diagonal torus;
• the dynamic unipotent subgroup is the positive root subgroup x₀₁.

The statements hold on points over every commutative algebra over the base ring. They are first expressed as concrete matrix membership criteria and then as equalities with the preimages of the standard matrix subgroups. They also show that every such point comes from the existing diagonal torus or root-subgroup point homomorphism. Thus the abstract dynamic decomposition agrees with the standard B = T U decomposition of GL₂.

The proofs specialize the general weight-cocharacter criteria for Levi and unipotent membership to the weights (1, 0), then identify the resulting matrix conditions with the standard diagonal torus and positive root subgroup.

Main declarations

• TauCeti.GeneralLinear.Dynamic.mem_dynamicLevi_iff: the dynamic Levi points are exactly the diagonal matrices.
• TauCeti.GeneralLinear.Dynamic.dynamicLevi_eq_diagonalTorus_comap: the dynamic Levi is the preimage of the diagonal torus under the matrix-point equivalence.
• TauCeti.GeneralLinear.Dynamic.mem_dynamicUnipotent_iff: the dynamic unipotent points are exactly the matrices !![1, b; 0, 1].
• TauCeti.GeneralLinear.Dynamic.dynamicUnipotent_eq_upperUnitriangularGroup_comap: the dynamic unipotent subgroup is the preimage of U₂ under the matrix-point equivalence.

References

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

This completes the concrete rank-one example in the dynamic parabolic/Levi route of Layer 7, "Structure theory", of the ReductiveGroups roadmap.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_dynamicLevi_iff {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) : g ∈ Cocharacter.levi A GL2.dynamicCocharacter ↔ (pointsMulEquiv 2) g ∈ TauCeti.diagonalTorus A 2

A point belongs to the dynamic Levi subgroup for t ↦ diag(t, 1) exactly when its matrix is diagonal.

theorem TauCeti.GeneralLinear.Dynamic.dynamicLevi_eq_diagonalTorus_comap {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] : Cocharacter.levi A GL2.dynamicCocharacter = Subgroup.comap (pointsMulEquiv 2).toMonoidHom (TauCeti.diagonalTorus A 2)

The dynamic Levi subgroup for t ↦ diag(t, 1) is the preimage of the diagonal torus under the general-linear point equivalence.

theorem TauCeti.GeneralLinear.Dynamic.mem_dynamicLevi_iff_exists_diagonalTorusPoint {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) : g ∈ Cocharacter.levi A GL2.dynamicCocharacter ↔ ∃ (q : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin 2) →₀ ℤ)) →ₐ[R] A)), diagonalTorusPoints q = g

A point belongs to the dynamic Levi subgroup exactly when it is the image of a point of the rank-two split torus.

@[simp]

theorem TauCeti.GeneralLinear.Dynamic.mem_dynamicUnipotent_iff {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) : g ∈ Cocharacter.unipotent A GL2.dynamicCocharacter ↔ ∃ (b : A), (pointsMulEquiv 2) g = Matrix.GeneralLinearGroup.upperRightHom b

A point belongs to the dynamic unipotent subgroup for t ↦ diag(t, 1) exactly when its matrix is !![1, b; 0, 1] for some b.

theorem TauCeti.GeneralLinear.Dynamic.dynamicUnipotent_eq_upperUnitriangularGroup_comap {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] : Cocharacter.unipotent A GL2.dynamicCocharacter = Subgroup.comap (pointsMulEquiv 2).toMonoidHom (upperUnitriangularGroup (Fin 2) A)

The dynamic unipotent subgroup for t ↦ diag(t, 1) is the preimage of the standard upper-unitriangular subgroup U₂ under the general-linear point equivalence.

theorem TauCeti.GeneralLinear.Dynamic.mem_dynamicUnipotent_iff_exists_rootSubgroupPoint {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) : g ∈ Cocharacter.unipotent A GL2.dynamicCocharacter ↔ ∃ (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)), (rootSubgroupPoints mem_dynamicUnipotent_iff_exists_rootSubgroupPoint._proof_1) q = g

A point belongs to the dynamic unipotent subgroup exactly when it comes from the positive simple-root point homomorphism x₀₁.