Cocharacters through a diagonalizable subgroup

Let π : H →ₐc[R] R[X] present a group morphism D(X) → G = Spec H from the diagonalizable group of a commutative group X, for instance a chosen split maximal torus. A cocharacter ψ : X →* Multiplicative ℤ of D(X) gives the cocharacter λ = π.cocharacter ψ of G, the composite 𝔾ₘ → D(X) → G. On points it sends a unit u to the image in G of the point of D(X) whose character is χ ↦ u ^ ⟨χ, ψ⟩.

Main declarations

• BialgHom.cocharacter: the cocharacter 𝔾ₘ → D(X) → G of a cocharacter of D(X), with point formula BialgHom.pointsHom_cocharacter.
• BialgHom.cocharacter_id_single: evaluation of a cocharacter on a group-algebra monomial.
• BialgHom.cocharacter_id_comp: composition with a diagonalizable-group cocharacter.
• BialgHom.ker_le_ker_cocharacter: the cocharacter kills the functions vanishing on D(X).
• BialgHom.pointsHom_cocharacter_mul and BialgHom.cocharacter_pow: products and powers of cocharacters of D(X).

References

• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, §2.1.

noncomputable def BialgHom.cocharacter {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (ψ : X →* Multiplicative ℤ) : H →ₐc[R] LaurentPolynomial R

The cocharacter 𝔾ₘ → D(X) → G given by a cocharacter ψ of the diagonalizable group D(X), where π presents the group morphism D(X) → G.

@[simp]

theorem BialgHom.toMultiplicativeBialgEquiv_comp_cocharacter {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (ψ : X →* Multiplicative ℤ) : (↑(AddMonoidAlgebra.toMultiplicativeBialgEquiv R R ℤ)).comp (π.cocharacter ψ) = (MonoidAlgebra.mapDomainBialgHom R ψ).comp π

In the group-algebra presentation of 𝔾ₘ, the cocharacter of ψ is π followed by the map of group algebras induced by ψ.

@[simp]

theorem BialgHom.cocharacter_id_single {R : Type u} {X : Type w} [CommRing R] [CommGroup X] (ψ : X →* Multiplicative ℤ) (χ : X) (r : R) : ((BialgHom.id R (MonoidAlgebra R X)).cocharacter ψ) (MonoidAlgebra.single χ r) = AddMonoidAlgebra.single (Multiplicative.toAdd (ψ χ)) r

A diagonalizable-group cocharacter sends a group-algebra monomial to the Laurent monomial with the same coefficient and the exponent specified by the cocharacter.

@[simp]

theorem BialgHom.cocharacter_id_comp {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (ψ : X →* Multiplicative ℤ) : ((BialgHom.id R (MonoidAlgebra R X)).cocharacter ψ).comp π = π.cocharacter ψ

Composing a diagonalizable-group cocharacter with π gives the cocharacter through π.

theorem BialgHom.ker_le_ker_cocharacter {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (ψ : X →* Multiplicative ℤ) : RingHom.ker (↑π).toRingHom ≤ RingHom.ker (↑(π.cocharacter ψ)).toRingHom

The cocharacter of ψ factors through D(X), so it kills every function vanishing on D(X).

Points

theorem BialgHom.pointsHom_cocharacter {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {A : Type x} [CommRing A] [Algebra R A] (ψ : X →* Multiplicative ℤ) (u : Aˣ) : (TauCeti.Cocharacter.pointsHom A (π.cocharacter ψ)) u = π.mapDomain ((TauCeti.DiagonalizableGroup.cocharPoints ψ) (TauCeti.DiagonalizableGroup.pointsMulEquiv.symm ((zpowersHom Aˣ) u)))

The cocharacter of ψ sends a unit u to the image in G of the point DiagonalizableGroup.cocharPoints ψ of D(X) at u, whose character is χ ↦ u ^ ⟨χ, ψ⟩.

theorem BialgHom.pointsHom_cocharacter_mul {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {A : Type x} [CommRing A] [Algebra R A] (ψ ψ' : X →* Multiplicative ℤ) (u : Aˣ) : (TauCeti.Cocharacter.pointsHom A (π.cocharacter (ψ * ψ'))) u = (TauCeti.Cocharacter.pointsHom A (π.cocharacter ψ)) u * (TauCeti.Cocharacter.pointsHom A (π.cocharacter ψ')) u

The product of two cocharacters of D(X) acts on points as the product of their actions.

theorem BialgHom.cocharacter_pow {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [Bialgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (ψ : X →* Multiplicative ℤ) (n : ℤ) : π.cocharacter (ψ ^ n) = (π.cocharacter ψ).powCocharacter n

The n-th power of a cocharacter of D(X) gives the n-th power t ↦ λ(tⁿ) of its cocharacter.