Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.Coordinate

The coordinate morphism of a finite free comodule #

A right comodule over a commutative Hopf algebra H with a basis indexed by Fin n has a coefficient matrix over H, whose determinant is a unit (TauCeti.Comodule.isUnit_det_coefficientMatrix). Evaluation on that matrix therefore extends from the matrix monoid coordinate ring to the coordinate ring of GLₙ, and the coalgebra identities satisfied by the coefficient matrix say exactly that the extension is a morphism of bialgebras

O(GLₙ) ⟶ H.

This is the coordinate-ring morphism opposite to the representation of the affine group represented by H on the chosen basis. Its surjectivity is the algebraic condition which the faithful-representation criterion identifies with a closed immersion into GLₙ.

Main declarations #

References #

This is the standard coordinate morphism of a finite free representation; see J. S. Milne, Algebraic Groups (2017), Chapter 4, especially Remark 4.1 and Theorem 4.9. It advances ReductiveGroups/README.md, Layer 1, "Faithfulness done right".

source
noncomputable def TauCeti.Comodule.coordinateBialgHom {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} (b : Module.Basis (Fin n) R M) :
↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐc[R] H

The coordinate Hopf-algebra morphism associated to a comodule with a basis indexed by Fin n.

Contravariantly, this is the morphism from the affine group represented by H to GLₙ defined by the corresponding representation.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.coordinateBialgHom_X {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} (b : Module.Basis (Fin n) R M) (i j : Fin n) :
    (coordinateBialgHom b) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.coordinateRingMap R n) (MvPolynomial.X (i, j)))) = coefficientMatrix b i j

    The coordinate Hopf-algebra morphism sends a generic matrix entry to the corresponding coefficient-matrix entry.

    source
    theorem AlgHom.pointsMulEquiv_comp_coordinateBialgHom {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [TauCeti.Comodule R H M] {n : ℕ} {K : Type x} [CommRing K] [Algebra R K] (f : H →ₐ[R] K) (b : Module.Basis (Fin n) R M) :
    ↑((TauCeti.GeneralLinear.pointsMulEquiv n) (WithConv.toConv (f.comp ↑(TauCeti.Comodule.coordinateBialgHom b)))) = (TauCeti.Comodule.coefficientMatrix b).map ⇑f

    Evaluating a representation's coordinate morphism through an algebra morphism gives its coefficient matrix mapped through that morphism.

    source
    @[simp]
    theorem TauCeti.Comodule.coordinateBialgHom_antipode_X {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} (b : Module.Basis (Fin n) R M) (i j : Fin n) :
    (coordinateBialgHom b) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((GeneralLinear.localizedGenericMatrix R n)⁻¹ i j)) = (HopfAlgebraStruct.antipode R) (coefficientMatrix b i j)

    The coordinate Hopf-algebra morphism sends an antipode generator of O(GLₙ) — an entry of the inverse of the localized generic matrix — to the antipode of the corresponding coefficient-matrix entry.

    source
    @[simp]
    theorem TauCeti.Comodule.coordinateBialgHom_corestrict {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} {K : Type x} [CommRing K] [HopfAlgebra R K] (f : H →ₐc[R] K) (b : Module.Basis (Fin n) R M) :
    coordinateBialgHom b = f.comp (coordinateBialgHom b)

    The coordinate morphism of a comodule corestricted along a bialgebra morphism is the composite of the original coordinate morphism with that bialgebra morphism.

    source
    @[simp]
    theorem TauCeti.Comodule.coordinateBialgHom_eq_unit_comp_counit_of_coact_eq_tmul_one {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} (b : Module.Basis (Fin n) R M) (htrivial : ∀ (m : M), coact m = m ⊗ₜ[R] 1) :
    coordinateBialgHom b = (Bialgebra.unitBialgHom R H).comp (Bialgebra.counitBialgHom R ↑(GeneralLinear.coordinateHopfAlgebra R n))

    If every vector has trivial coaction, the coordinate morphism of the representation factors through the counit of O(GLₙ) and the unit of the coefficient Hopf algebra.