Documentation

TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Subcoalgebra

The coefficient subcoalgebra of a finite free comodule #

Expanding the comultiplication of a matrix coefficient in a finite basis (eᵢ) gives

Δ(c(φ, m)) = ∑ i, c(φ, eᵢ) ⊗ c(eⁱ, m).

Consequently, over a commutative semiring, the matrix-coefficient submodule of a finite free comodule is finite and stable under comultiplication, and hence defines a finite subcoalgebra.

Main declarations #

References #

This is the standard coefficient-coalgebra construction; see Sweedler, Hopf Algebras, Chapter 2.

source
noncomputable def TauCeti.Comodule.matrixCoefficientSubcoalgebra {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] :
Subcoalgebra R C

The subcoalgebra spanned by the matrix coefficients of a finite free comodule.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.matrixCoefficientSubcoalgebra_toSubmodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] :
    matrixCoefficientSubcoalgebra.toSubmodule = matrixCoefficientSubmodule

    The underlying submodule of the coefficient subcoalgebra is the matrix-coefficient submodule.

    source
    instance TauCeti.Comodule.matrixCoefficientSubcoalgebra_finite {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] :
    Module.Finite R ↥matrixCoefficientSubcoalgebra.toSubmodule

    The underlying module of the coefficient subcoalgebra of a finite free comodule is finite.

    source
    @[simp]
    theorem TauCeti.Comodule.mem_matrixCoefficientSubcoalgebra {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] {c : C} :
    c ∈ matrixCoefficientSubcoalgebra ↔ c ∈ matrixCoefficientSubmodule

    Membership in the coefficient subcoalgebra is membership in the matrix-coefficient submodule.

    source
    theorem TauCeti.Comodule.matrixCoefficient_mem_subcoalgebra {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] (φ : Module.Dual R M) (m : M) :
    matrixCoefficient φ m ∈ matrixCoefficientSubcoalgebra

    Every matrix coefficient belongs to the coefficient subcoalgebra.

    This is not a simp lemma: mem_matrixCoefficientSubcoalgebra and matrixCoefficient_mem_submodule already discharge the goal, and tagging it would make it simpNF-redundant.

    source
    theorem TauCeti.Comodule.matrixCoefficientSubcoalgebra_le {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] {D : Subcoalgebra R C} (hD : ∀ (φ : Module.Dual R M) (m : M), matrixCoefficient φ m ∈ D) :
    matrixCoefficientSubcoalgebra ≤ D

    The coefficient subcoalgebra is the smallest subcoalgebra containing all matrix coefficients.

    source
    theorem TauCeti.Comodule.matrixCoefficientSubcoalgebra_le_iff {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Free R M] [Module.Finite R M] {D : Subcoalgebra R C} :
    matrixCoefficientSubcoalgebra ≤ D ↔ ∀ (φ : Module.Dual R M) (m : M), matrixCoefficient φ m ∈ D

    The coefficient subcoalgebra is contained in a subcoalgebra exactly when that subcoalgebra contains every matrix coefficient.