Opposite dynamic parabolics #
The cocharacter opposite to λ is t ↦ λ(t⁻¹). The intersection of the dynamic parabolics
of these two cocharacters is their common Levi subgroup. This holds over every commutative
value semiring: a Laurent-valued conjugation family that extends over both ends has only
its constant coefficient, so it centralizes the cocharacter.
This identifies the Levi as an intersection of closed subgroups, without reductivity or
smoothness assumptions. The negative-coefficient criterion is
TauCeti.Cocharacter.mem_parabolic_iff_forall_coeff_conjugate_eq_zero.
References #
- B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.
- J. S. Milne, Algebraic Groups (2017), Chapter 13.
theorem
TauCeti.Cocharacter.conjugate_oppositeCocharacter
{R : Type u_1}
{H : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring H]
[HopfAlgebra R H]
[CommSemiring A]
[Algebra R A]
(l : H →ₐc[R] LaurentPolynomial R)
(g : WithConv (H →ₐ[R] A))
:
(conjugate A l.oppositeCocharacter) g = (AlgHom.restrictScalars R ↑LaurentPolynomial.invert).mapValue ((conjugate A l) g)
Reversing the cocharacter inverts the variable of the conjugation family.
@[simp]
theorem
TauCeti.Cocharacter.levi_oppositeCocharacter
{R : Type u_1}
{H : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring H]
[HopfAlgebra R H]
[CommSemiring A]
[Algebra R A]
(l : H →ₐc[R] LaurentPolynomial R)
:
Opposite cocharacters have the same Levi subgroup.
@[simp]
theorem
TauCeti.Cocharacter.parabolic_inf_oppositeCocharacter
{R : Type u_1}
{H : Type u_2}
{A : Type u_3}
[CommSemiring R]
[Semiring H]
[HopfAlgebra R H]
[CommSemiring A]
[Algebra R A]
(l : H →ₐc[R] LaurentPolynomial R)
:
The two opposite dynamic parabolics meet exactly in their common Levi subgroup.