Documentation

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Scheme.GeneralLinear

Diagonal representations of a diagonalizable group #

A weight function wt : Fin n → G on a basis of a free module M makes M a comodule over the group algebra R[G], that is, a representation of the diagonalizable group D(G) which is diagonal in that basis. This file records the resulting morphism of affine group schemes

D(G) ⟶ GLₙ

and a sufficient condition for it to be a closed immersion: the weights generate the character group G. Indeed, their group-algebra generators then lie in the range of the coordinate morphism O(GLₙ) ⟶ R[G], making that morphism surjective and the representation faithful.

For G = ℤ^κ this is the split torus 𝔾ₘ^κ presented as a closed subgroup of GLₙ by the weights of a representation, which is how the split maximal torus of a Chevalley group is written down.

Main declarations #

Main results #

References #

The coordinate morphism of a diagonal representation #

source
noncomputable def TauCeti.DiagonalizableGroup.diagonalCoordinateMap {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) :
↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐc[R] MonoidAlgebra R G

The coordinate Hopf-algebra morphism O(GLₙ) ⟶ R[G] of the representation of D(G) which is diagonal in the basis b with weights wt.

Equations
Instances For
    source
    theorem TauCeti.DiagonalizableGroup.diagonalCoordinateMap_X {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) (i j : Fin n) :
    (diagonalCoordinateMap b wt) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.coordinateRingMap R n) (MvPolynomial.X (i, j)))) = Matrix.diagonal (fun (x : Fin n) => MonoidAlgebra.single (wt x) 1) i j

    The coordinate morphism of a diagonal representation sends the generic matrix to the diagonal matrix of the characters.

    source
    theorem TauCeti.DiagonalizableGroup.diagonalCoordinateMap_antipode_X {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) (i j : Fin n) :
    (diagonalCoordinateMap b wt) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.localizedGenericMatrix R n)⁻¹ i j)) = Matrix.diagonal (fun (x : Fin n) => MonoidAlgebra.single (wt x)⁻¹ 1) i j

    The antipode generators of O(GLₙ) are sent to the inverse characters.

    source
    theorem TauCeti.DiagonalizableGroup.pointToGeneralLinear_comp_diagonalCoordinateMap {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] {A : Type u_1} [CommRing A] [Algebra R A] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) (q : WithConv (MonoidAlgebra R G →ₐ[R] A)) :
    ↑(GeneralLinear.pointToGeneralLinear n (WithConv.toConv (q.ofConv.comp ↑(diagonalCoordinateMap b wt)))) = Matrix.diagonal fun (x : Fin n) => ↑((charOfPoint q.ofConv) (wt x))

    On points, a diagonal representation is the diagonal matrix of the values of its weights. A point of D(G) is a character χ of G, and it acts on the x-th basis vector by χ (wt x).

    Faithfulness #

    source
    theorem TauCeti.DiagonalizableGroup.single_mem_range_diagonalCoordinateMap {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) {g : G} (hg : g ∈ Subgroup.closure (Set.range wt)) :
    MonoidAlgebra.single g 1 ∈ (↑(diagonalCoordinateMap b wt)).range

    Every generator of the group algebra whose character is generated by the weights lies in the range of the coordinate morphism.

    source
    theorem TauCeti.DiagonalizableGroup.surjective_diagonalCoordinateMap {R : Type u} {G : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommGroup G] [AddCommMonoid M] [Module R M] (b : Module.Basis (Fin n) R M) (wt : Fin n → G) (hwt : Subgroup.closure (Set.range wt) = ⊤) :
    Function.Surjective ⇑(diagonalCoordinateMap b wt)

    A diagonal representation whose weights generate the character group is faithful: its coordinate morphism O(GLₙ) ⟶ R[G] is surjective.

    The morphism of group schemes #

    source
    noncomputable def TauCeti.DiagonalizableGroup.diagonalGroupSchemeHom {R M : Type u} {n : ℕ} [CommRing R] [AddCommMonoid M] [Module R M] (G : FGCommGrpCat) (b : Module.Basis (Fin n) R M) (wt : Fin n → ↑G) :
    groupScheme R G ⟶ GeneralLinear.groupScheme R n

    The morphism of affine group schemes D(G) ⟶ GLₙ attached to the representation of D(G) which is diagonal in the basis b with weights wt.

    Equations
    Instances For
      source
      theorem TauCeti.DiagonalizableGroup.diagonalGroupSchemeHom_def {R M : Type u} {n : ℕ} [CommRing R] [AddCommMonoid M] [Module R M] (G : FGCommGrpCat) (b : Module.Basis (Fin n) R M) (wt : Fin n → ↑G) :
      diagonalGroupSchemeHom G b wt = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom (diagonalCoordinateMap b wt)).op) (CategoryTheory.eqToHom ⋯))

      The diagonal group-scheme morphism is relative spectrum applied contravariantly to its coordinate morphism, transported across the named presentation of D(G).

      source
      theorem TauCeti.DiagonalizableGroup.isClosedImmersion_diagonalGroupSchemeHom {R M : Type u} {n : ℕ} [CommRing R] [AddCommMonoid M] [Module R M] (G : FGCommGrpCat) (b : Module.Basis (Fin n) R M) (wt : Fin n → ↑G) (hwt : Subgroup.closure (Set.range wt) = ⊤) :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (diagonalGroupSchemeHom G b wt).hom.hom)

      A diagonal representation whose weights generate the character group presents D(G) as a closed subgroup of GLₙ.