Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.UpperUnitriangular

Representations with upper-unitriangular coefficient matrices #

Let M be a finite free comodule over a commutative Hopf algebra H. If the coefficient matrix of M in a basis b is upper unitriangular, evaluation at its strict-upper entries defines a coordinate Hopf-algebra morphism

O(U_n) ⟶ H.

This morphism factors the usual coordinate morphism O(GL_n) ⟶ H through the quotient O(GL_n) ⟶ O(U_n). Consequently, if M is faithful, the represented affine group embeds as a closed subgroup of U_n.

This is the coordinate-algebra bridge needed for the upper-unitriangular embedding characterization in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. The remaining Kolchin step must produce a basis with upper-unitriangular coefficient matrix for a faithful representation of a unipotent group.

Main declarations #

References #

source
noncomputable def TauCeti.Comodule.upperUnitriangularCoordinateBialgHom {R : Type u} {H : Type v} {M : Type w} {m : Type x} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
↑(UpperUnitriangular.coordinateHopfAlgebra R m) →ₐc[R] H

The coordinate Hopf-algebra morphism of a comodule whose coefficient matrix is upper unitriangular in the chosen basis. It sends each strict-upper coordinate of U_n to the corresponding matrix coefficient.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.upperUnitriangularCoordinateBialgHom_X {R : Type u} {H : Type v} {M : Type w} {m : Type x} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) (ij : UpperUnitriangular.Index m) :
    (upperUnitriangularCoordinateBialgHom b h) ((UpperUnitriangular.coordinateHopfAlgebraAlgEquiv R m) (MvPolynomial.X ij)) = coefficientMatrix b (↑ij).1 (↑ij).2

    The upper-unitriangular coordinate morphism sends each strict-upper coordinate generator to the corresponding coefficient-matrix entry.

    source
    @[simp]
    theorem TauCeti.Comodule.upperUnitriangularCoordinateBialgHom_genericMatrix_apply {R : Type u} {H : Type v} {M : Type w} {m : Type x} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) (i j : m) :
    (upperUnitriangularCoordinateBialgHom b h) ((UpperUnitriangular.coordinateHopfAlgebraAlgEquiv R m) (UpperUnitriangular.genericMatrix R m i j)) = coefficientMatrix b i j

    The upper-unitriangular coordinate morphism sends every entry of the generic matrix to the corresponding coefficient-matrix entry.

    source
    theorem TauCeti.Comodule.upperUnitriangularCoordinateBialgHom_comp_coordinateMap {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
    (upperUnitriangularCoordinateBialgHom b h).comp (CommHopfAlgCat.Hom.hom (UpperUnitriangular.coordinateMap R n)) = coordinateBialgHom b

    The coordinate morphism of an upper-unitriangular representation factors the ordinary general-linear coordinate morphism through O(U_n).

    source
    theorem TauCeti.Comodule.upperUnitriangularCoordinateBialgHom_surjective_of_coordinateBialgHom_surjective {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) (h : (coefficientMatrix b).IsUpperUnitriangular) (hsurj : Function.Surjective ⇑(coordinateBialgHom b)) :
    Function.Surjective ⇑(upperUnitriangularCoordinateBialgHom b h)

    If the ordinary coordinate morphism of an upper-unitriangular representation is surjective, then its factored coordinate morphism O(U_n) ⟶ H is surjective.

    source
    theorem TauCeti.Comodule.upperUnitriangularCoordinateBialgHom_surjective_iff_isFaithful {R H M : Type u} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
    Function.Surjective ⇑(upperUnitriangularCoordinateBialgHom b h) ↔ IsFaithful

    The upper-unitriangular coordinate morphism is surjective exactly when the comodule is faithful.

    source
    noncomputable def TauCeti.Comodule.upperUnitriangularCoordinateGroupSchemeHom {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {m : Type} [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
    (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op ↧H) ⟶ UpperUnitriangular.groupScheme R m

    The morphism from the affine group represented by H to the upper-unitriangular group associated to a basis in which the coefficient matrix is upper unitriangular.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.Comodule.upperUnitriangularCoordinateGroupSchemeHom_def {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {m : Type} [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
      upperUnitriangularCoordinateGroupSchemeHom b h = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom (upperUnitriangularCoordinateBialgHom b h)).op) (CategoryTheory.eqToHom ⋯)

      The upper-unitriangular representation morphism is relative spectrum applied to its coordinate morphism, followed by the defining identification of the upper-unitriangular group.

      source
      theorem TauCeti.Comodule.upperUnitriangularCoordinateGroupSchemeHom_comp_inclusion {R H M : Type u} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
      CategoryTheory.CategoryStruct.comp (upperUnitriangularCoordinateGroupSchemeHom b h) (UpperUnitriangular.inclusion R n) = coordinateGroupSchemeHom b

      Composing the upper-unitriangular representation with U_n ⟶ GL_n recovers the usual general-linear representation.

      source
      @[simp]
      theorem TauCeti.Comodule.isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom_iff {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {m : Type} [Fintype m] [LinearOrder m] (b : Module.Basis m R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (upperUnitriangularCoordinateGroupSchemeHom b h).hom.hom) ↔ Function.Surjective ⇑(upperUnitriangularCoordinateBialgHom b h)

      The upper-unitriangular representation morphism is a closed immersion exactly when its coordinate Hopf-algebra morphism is surjective.

      source
      theorem TauCeti.Comodule.isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom_iff_isFaithful {R H M : Type u} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) (h : (coefficientMatrix b).IsUpperUnitriangular) :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (upperUnitriangularCoordinateGroupSchemeHom b h).hom.hom) ↔ IsFaithful

      The morphism into U_n defined by an upper-unitriangular coefficient matrix is a closed immersion exactly when the comodule is faithful.