Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.GL2.Basic

The upper-triangular Borel as a dynamic parabolic of GL₂ #

For the cocharacter

lambda(t) = diag(t, 1)

of GL₂, conjugation sends a matrix !![a, b; c, d] to !![a, tb; t⁻¹c, d]. Consequently the conjugate extends from the punctured affine line across the origin exactly when c = 0: the dynamic parabolic P(lambda) is the upper-triangular Borel. For such a matrix the limit at the origin is its diagonal part.

The file specializes TauCeti.GeneralLinear.weightCocharacter at the weights (1, 0). Thus the result holds over every commutative base ring and every commutative value algebra, including rings with zero divisors.

Main declarations #

References #

This supplies the explicit GL₂ check for the dynamic-parabolic route in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

source
noncomputable def TauCeti.GeneralLinear.Dynamic.GL2.dynamicCocharacter {R : Type u} [CommRing R] :
↑(coordinateHopfAlgebra R 2) →ₐc[R] LaurentPolynomial R

The bialgebra morphism representing the standard cocharacter t ↦ diag(t, 1).

Equations
Instances For
    source
    theorem TauCeti.GeneralLinear.Dynamic.GL2.dynamicCocharacter_eq_weightCocharacter {R : Type u} [CommRing R] :
    dynamicCocharacter = weightCocharacter Borel.weights

    The standard dynamic cocharacter is the weight cocharacter for weights (1, 0).

    source
    @[simp]
    theorem TauCeti.GeneralLinear.Dynamic.GL2.mem_dynamicParabolic_iff {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) :
    g ∈ Cocharacter.parabolic A dynamicCocharacter ↔ (pointsMulEquiv 2) g ∈ GL2Borel A

    Membership in the dynamic parabolic for t ↦ diag(t, 1) is exactly upper triangularity.

    source
    theorem TauCeti.GeneralLinear.Dynamic.GL2.pointsMulEquiv_limit_dynamicCocharacter {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) (hg : g ∈ Cocharacter.parabolic A dynamicCocharacter) :
    (pointsMulEquiv 2) ((Cocharacter.limit A dynamicCocharacter) ⟨g, hg⟩) = ↑(GL2Borel.torusHom (GL2Borel.diag ⟨(pointsMulEquiv 2) g, ⋯⟩))

    The dynamic limit of an upper-triangular matrix is its diagonal part.

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

    As subgroups of convolution points, the dynamic parabolic for t ↦ diag(t, 1) is the preimage of the upper-triangular Borel under the general-linear point equivalence.