Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.MultiplicativeMatrix

Coordinate morphisms out of GLₙ determined by a multiplicative matrix #

A square matrix Y over a commutative Hopf algebra S is multiplicative when

Y.map Δ = (Y ⊗ 1) (1 ⊗ Y),   Y.map ε = 1,

that is, when each entry comultiplies as Δ Yᵢⱼ = ∑ₖ Yᵢₖ ⊗ Yₖⱼ and counits to the corresponding entry of the identity matrix. The generic matrix satisfies these identities, and transporting it along a bialgebra morphism preserves them. Conversely, a multiplicative matrix determines a morphism of commutative Hopf algebras

O(GLₙ) →ₐc[R] S

carrying the generic matrix to Y. Contravariantly, a multiplicative matrix over the coordinate Hopf algebra of an affine group scheme G is the same thing as a homomorphism G → GLₙ, hence the same thing as an n-dimensional representation of G; the conditions say that the matrix is multiplicative and unital on points, functorially in the value algebra.

The determinant of a multiplicative matrix is automatically invertible — it is a group-like element of S — so no separate hypothesis is needed to land in GLₙ rather than in the matrix monoid.

The matrix-to-comodule construction lives in TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.FromMatrix. This file applies it to obtain the coordinate morphism. The coordinate algebra of GLₙ inverts the determinant, and the entries of the inverse matrix are received through the antipode, so the target is required to be a Hopf algebra.

Main declarations #

References #

The standard comodule TauCeti.GeneralLinear.standardComodule is obtained by specializing this construction to the generic matrix.

The generic matrix transported along a coordinate morphism #

source
@[simp]
theorem TauCeti.GeneralLinear.map_comul_map_genericMatrix {R : Type u} {n : ℕ} [CommRing R] {S : Type v} [Semiring S] [Bialgebra R S] (φ : ↑(coordinateHopfAlgebra R n) →ₐc[R] S) :
(genericMatrix R n).map (⇑(Bialgebra.comulAlgHom R S) ∘ ⇑φ) = ((genericMatrix R n).map ⇑φ).map ⇑Algebra.TensorProduct.includeLeft * ((genericMatrix R n).map ⇑φ).map ⇑Algebra.TensorProduct.includeRight

The comultiplication condition for the generic matrix transported along a morphism of commutative bialgebras. The image of the generic matrix under any such morphism is multiplicative, since the generic matrix is and the morphism respects comultiplication.

source
@[simp]
theorem TauCeti.GeneralLinear.map_counit_map_genericMatrix {R : Type u} {n : ℕ} [CommRing R] {S : Type v} [Semiring S] [Bialgebra R S] (φ : ↑(coordinateHopfAlgebra R n) →ₐc[R] S) :
(genericMatrix R n).map (⇑(Bialgebra.counitAlgHom R S) ∘ ⇑φ) = 1

The counit condition for the generic matrix transported along a morphism of commutative bialgebras.

The coordinate morphism of a multiplicative matrix #

The coordinate algebra of GLₙ inverts the determinant, so a morphism out of it needs the antipode of S to receive the entries of the inverse matrix; this part asks for a Hopf algebra.

source
noncomputable def TauCeti.GeneralLinear.coordinateBialgHomOfMultiplicative (R : Type u) (n : ℕ) [CommRing R] {S : Type v} [CommRing S] [HopfAlgebra R S] (Y : Matrix (Fin n) (Fin n) S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) :
↑(coordinateHopfAlgebra R n) →ₐc[R] S

The coordinate morphism of a multiplicative matrix: the morphism of commutative Hopf algebras out of the coordinate algebra of GL n sending the generic matrix to Y.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.coordinateBialgHomOfMultiplicative_X (R : Type u) (n : ℕ) [CommRing R] {S : Type v} [CommRing S] [HopfAlgebra R S] (Y : Matrix (Fin n) (Fin n) S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) (i j : Fin n) :
    (coordinateBialgHomOfMultiplicative R n Y hcomul hcounit) ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = Y i j

    The coordinate morphism of a multiplicative matrix sends a generic matrix entry to the corresponding entry of the matrix.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.coordinateBialgHomOfMultiplicative_antipode_X (R : Type u) (n : ℕ) [CommRing R] {S : Type v} [CommRing S] [HopfAlgebra R S] (Y : Matrix (Fin n) (Fin n) S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) (i j : Fin n) :
    (coordinateBialgHomOfMultiplicative R n Y hcomul hcounit) ((coordinateHopfAlgebraAlgEquiv R n) ((localizedGenericMatrix R n)⁻¹ i j)) = (HopfAlgebraStruct.antipode R) (Y i j)

    The coordinate morphism of a multiplicative matrix sends an inverse generic-matrix entry to the antipode of the corresponding matrix entry.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.map_genericMatrix_coordinateBialgHomOfMultiplicative (R : Type u) (n : ℕ) [CommRing R] {S : Type v} [CommRing S] [HopfAlgebra R S] (Y : Matrix (Fin n) (Fin n) S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) :
    (genericMatrix R n).map ⇑(coordinateBialgHomOfMultiplicative R n Y hcomul hcounit) = Y

    The coordinate morphism of a multiplicative matrix carries the generic matrix to that matrix.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.coordinateBialgHomOfMultiplicative_map_genericMatrix (R : Type u) (n : ℕ) [CommRing R] {S : Type v} [CommRing S] [HopfAlgebra R S] (φ : ↑(coordinateHopfAlgebra R n) →ₐc[R] S) :
    coordinateBialgHomOfMultiplicative R n ((genericMatrix R n).map ⇑φ) ⋯ ⋯ = φ

    Reconstructing a bialgebra morphism from its image of the generic matrix returns the original morphism.