Documentation

TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.FromMatrix

A comodule reconstructed from a multiplicative matrix #

A square matrix whose entries satisfy the matrix comultiplication and counit identities defines a coaction on a finite free module. Its coefficient matrix is the original matrix, so this reverses the coefficient-matrix construction.

Main declarations #

The comodule of a multiplicative matrix #

Only the comultiplication and counit of S are used here, so this part asks for a bialgebra.

source
noncomputable def TauCeti.Comodule.matrixCoact (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [AddCommMonoid S] [Module R S] (Y : Matrix ι ι S) :
(ι → R) →ₗ[R] TensorProduct R (ι → R) S

The candidate coaction on column vectors determined by a square matrix over an R-module: the jth basis vector goes to the jth column of the matrix. This is a linear map for an arbitrary matrix; the coassociativity and counit laws that make it a coaction come from the multiplicativity hypotheses of TauCeti.Comodule.matrixComodule.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.matrixCoact_apply_basisFun (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [AddCommMonoid S] [Module R S] (Y : Matrix ι ι S) (j : ι) :
    (matrixCoact R Y) ((Pi.basisFun R ι) j) = ∑ i : ι, (Pi.basisFun R ι) i ⊗ₜ[R] Y i j

    The candidate coaction of a matrix takes a basis vector to the corresponding column.

    source
    theorem TauCeti.Comodule.map_comul_iff (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) :
    Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight ↔ ∀ (i j : ι), CoalgebraStruct.comul (Y i j) = ∑ k : ι, Y i k ⊗ₜ[R] Y k j

    The matrix comultiplication condition is equivalent to its entrywise form.

    source
    theorem TauCeti.Comodule.map_counit_iff (R : Type u) {ι : Type u_1} [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) [DecidableEq ι] :
    Y.map ⇑(Bialgebra.counitAlgHom R S) = 1 ↔ ∀ (i j : ι), CoalgebraStruct.counit (Y i j) = if i = j then 1 else 0

    The matrix counit condition is equivalent to its entrywise form.

    source
    theorem TauCeti.Comodule.map_comul_map (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) {T : Type w} [Semiring T] [Bialgebra R T] (f : S →ₐc[R] T) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) :
    (Y.map ⇑f).map ⇑(Bialgebra.comulAlgHom R T) = (Y.map ⇑f).map ⇑Algebra.TensorProduct.includeLeft * (Y.map ⇑f).map ⇑Algebra.TensorProduct.includeRight

    A morphism of bialgebras carries the matrix comultiplication condition to the entrywise image of the matrix.

    source
    theorem TauCeti.Comodule.map_counit_map (R : Type u) {ι : Type u_1} [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) {T : Type w} [Semiring T] [Bialgebra R T] (f : S →ₐc[R] T) [DecidableEq ι] (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) :
    (Y.map ⇑f).map ⇑(Bialgebra.counitAlgHom R T) = 1

    A morphism of bialgebras carries the matrix counit condition to the entrywise image of the matrix.

    source
    theorem TauCeti.Comodule.counit_basisFun_of_map_counit (R : Type u) {ι : Type u_1} [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) [Finite ι] [DecidableEq ι] (hcounit : Y.map ⇑(Bialgebra.counitAlgHom R S) = 1) (i j : ι) :
    CoalgebraStruct.counit (Y i j) = ((Pi.basisFun R ι).repr ((Pi.basisFun R ι) j)) i

    The matrix counit identity gives the basis-coordinate form needed to construct a comodule. This form does not expose a decidable-equality requirement on the reconstructed comodule.

    source
    @[instance_reducible]
    noncomputable def TauCeti.Comodule.matrixComodule (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : ∀ (i j : ι), CoalgebraStruct.counit (Y i j) = ((Pi.basisFun R ι).repr ((Pi.basisFun R ι) j)) i) :
    Comodule R S (ι → R)

    A multiplicative matrix makes the column space a comodule.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Comodule.matrixComodule_coact (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : ∀ (i j : ι), CoalgebraStruct.counit (Y i j) = ((Pi.basisFun R ι).repr ((Pi.basisFun R ι) j)) i) :
      coact = matrixCoact R Y

      The coaction of the comodule of a multiplicative matrix is that matrix's coaction. This is the unfolding lemma through which the comodule's matrix coefficients are computed.

      source
      @[simp]
      theorem TauCeti.Comodule.coefficientMatrix_matrixComodule (R : Type u) {ι : Type u_1} [Fintype ι] [CommSemiring R] {S : Type v} [Semiring S] [Bialgebra R S] (Y : Matrix ι ι S) (hcomul : Y.map ⇑(Bialgebra.comulAlgHom R S) = Y.map ⇑Algebra.TensorProduct.includeLeft * Y.map ⇑Algebra.TensorProduct.includeRight) (hcounit : ∀ (i j : ι), CoalgebraStruct.counit (Y i j) = ((Pi.basisFun R ι).repr ((Pi.basisFun R ι) j)) i) :
      coefficientMatrix (Pi.basisFun R ι) = Y

      The coefficient matrix of the comodule of a multiplicative matrix is that matrix.