Documentation

TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Matrix

The coefficient matrix of a comodule with a finite basis #

For a right comodule M over C with a finite basis (eⱼ) and coordinate functionals (eⁱ), the matrix coefficients c(eⁱ, eⱼ) assemble into a square matrix over C. The comodule laws say that this matrix is multiplicative under comultiplication and specializes to the identity matrix under the counit.

When C is a Hopf algebra, the antipode identities say that the entrywise antipode transform is a two-sided inverse of the coefficient matrix; over a commutative Hopf algebra its determinant is therefore a unit.

Main declarations #

References #

This is the standard coefficient matrix of a finite free corepresentation; see Sweedler, Hopf Algebras, Chapter 2, and Milne, Algebraic Groups (2017), Chapter 4, Remark 4.1. It supplies a prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "Faithfulness done right".

source
noncomputable def TauCeti.Comodule.coefficientMatrix {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] (b : Module.Basis ι R M) :
Matrix ι ι C

The matrix of basis matrix coefficients of a comodule.

If eⱼ is a basis and eⁱ its coordinate functionals, the (i, j) entry is c(eⁱ, eⱼ).

Equations
Instances For
    source
    theorem TauCeti.Comodule.coefficientMatrix_apply {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] (b : Module.Basis ι R M) (i j : ι) :
    coefficientMatrix b i j = matrixCoefficient (b.coord i) (b j)

    An entry of the coefficient matrix is the corresponding basis matrix coefficient.

    This is not a simp lemma: the coefficient matrix is the normal form, and the coalgebra identities below are stated for its entries.

    source
    @[simp]
    theorem TauCeti.Comodule.coefficientMatrix_corestrict {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] {D : Type u_1} [AddCommMonoid D] [Module R D] [Coalgebra R D] (b : Module.Basis ι R M) (f : C →ₗc[R] D) :
    coefficientMatrix b = (coefficientMatrix b).map ⇑f

    Corestricting a comodule along a coalgebra morphism maps that morphism over every entry of the coefficient matrix.

    source
    @[simp]
    theorem TauCeti.Comodule.counit_coefficientMatrix {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] [DecidableEq ι] (b : Module.Basis ι R M) (i j : ι) :
    CoalgebraStruct.counit (coefficientMatrix b i j) = if i = j then 1 else 0

    The counit of a coefficient entry is the corresponding identity-matrix entry.

    source
    theorem TauCeti.Comodule.coact_basis_eq_sum_coefficientMatrix {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] [Fintype ι] (b : Module.Basis ι R M) (j : ι) :
    coact (b j) = ∑ i : ι, b i ⊗ₜ[R] coefficientMatrix b i j

    The coaction of a basis vector is its column in the coefficient matrix.

    source
    @[simp]
    theorem TauCeti.Comodule.comul_coefficientMatrix_eq_sum {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Comodule R C M] [Fintype ι] (b : Module.Basis ι R M) (i j : ι) :
    CoalgebraStruct.comul (coefficientMatrix b i j) = ∑ k : ι, coefficientMatrix b i k ⊗ₜ[R] coefficientMatrix b k j

    Comultiplication of a coefficient entry is matrix multiplication across the two tensor factors.

    source
    theorem TauCeti.Comodule.sum_matrixCoefficient_mul_antipode_eq_algebraMap {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [HopfAlgebra R C] [Comodule R C M] [Fintype ι] (b : Module.Basis ι R M) (p q : ι) :
    ∑ x : ι, matrixCoefficient (b.coord p) (b x) * (HopfAlgebraStruct.antipode R) (matrixCoefficient (b.coord x) (b q)) = (algebraMap R C) ((b.coord p) (b q))

    Multiplying the matrix of basis coefficients by its entrywise antipode transform gives the image under algebraMap of a single basis coordinate: taking p and q basis indices, the right-hand side is 1 when they agree and 0 otherwise.

    source
    theorem TauCeti.Comodule.sum_antipode_mul_matrixCoefficient_eq_algebraMap {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [HopfAlgebra R C] [Comodule R C M] [Fintype ι] (b : Module.Basis ι R M) (p q : ι) :
    ∑ x : ι, (HopfAlgebraStruct.antipode R) (matrixCoefficient (b.coord p) (b x)) * matrixCoefficient (b.coord x) (b q) = (algebraMap R C) ((b.coord p) (b q))

    The opposite multiplication order of sum_matrixCoefficient_mul_antipode_eq_algebraMap: the entrywise antipode transform is also a left inverse of the matrix of basis coefficients.

    source
    @[simp]
    theorem TauCeti.Comodule.coefficientMatrix_mul_map_antipode {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [HopfAlgebra R C] [Comodule R C M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) :
    coefficientMatrix b * (coefficientMatrix b).map ⇑(HopfAlgebraStruct.antipode R) = 1

    The entrywise antipode of the coefficient matrix is a right inverse.

    source
    @[simp]
    theorem TauCeti.Comodule.map_antipode_mul_coefficientMatrix {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring C] [HopfAlgebra R C] [Comodule R C M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) :
    (coefficientMatrix b).map ⇑(HopfAlgebraStruct.antipode R) * coefficientMatrix b = 1

    The entrywise antipode of the coefficient matrix is a left inverse.

    source
    theorem TauCeti.Comodule.isUnit_det_coefficientMatrix {R : Type u} {C : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommRing C] [HopfAlgebra R C] [Comodule R C M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) :
    IsUnit (coefficientMatrix b).det

    The determinant of the coefficient matrix is a unit.