Matrix coefficients of group-like and trivial comodules

This file packages the generated coefficient objects for group-like and trivial comodules. The group-like results hold over coalgebras, with algebra-generation statements requiring only an ambient compatible algebra structure. The individual coefficient calculations are already in TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Basic: if M has a group-like coaction attached to g, then every coefficient is a scalar multiple of g, and for the trivial coaction every coefficient is a scalar multiple of 1.

Here we record the corresponding span and algebra-generation consequences. For an arbitrary group-like module, its coefficient submodule is contained in the line spanned by g, and for the rank-one group-like comodule R, this inclusion is an equality. The corresponding coefficient subalgebra is contained in the subalgebra generated by g, and is exactly that subalgebra for the rank-one group-like comodule. Specializing directly to the trivial coefficient calculation, a trivial comodule's coefficient subalgebra is the bottom R-subalgebra.

This is Layer 1 infrastructure for the reductive-groups roadmap target "Faithfulness done right": the faithful-representation criterion is stated in terms of the algebra generated by matrix coefficients, and the tensor-unit/trivial representation should have the expected coefficient algebra.

Main declarations

• TauCeti.Comodule.groupLike_matrixCoefficientSubmodule_le_span_singleton.
• TauCeti.Comodule.groupLike_rankOne_matrixCoefficientSubmodule_eq_span_singleton.
• TauCeti.Comodule.groupLike_matrixCoefficientSubalgebra_le_adjoin_singleton.
• TauCeti.Comodule.groupLike_rankOne_matrixCoefficientSubalgebra_eq_adjoin_singleton.
• TauCeti.Comodule.trivial_rankOne_matrixCoefficientSubmodule_eq_span_singleton_one.
• TauCeti.Comodule.trivial_matrixCoefficientSubalgebra_le_bot.
• TauCeti.Comodule.trivial_matrixCoefficientSubalgebra_eq_bot.

References

These are the standard coefficient calculations for group-like and trivial comodules, using the existing Tau Ceti matrix-coefficient API and Mathlib's Algebra.adjoin/Submodule.span API.

theorem TauCeti.Comodule.groupLike_matrixCoefficient_mem_span_singleton {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (g : GroupLike R C) (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m ∈ R ∙ ↑g

A matrix coefficient of a group-like comodule lies in the line spanned by its group-like element.

theorem TauCeti.Comodule.groupLike_matrixCoefficientSubmodule_le_span_singleton {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (g : GroupLike R C) : matrixCoefficientSubmodule ≤ R ∙ ↑g

The coefficient submodule of a group-like comodule is contained in the line spanned by its group-like element.

theorem TauCeti.Comodule.groupLike_mem_rankOne_matrixCoefficientSet {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : ↑g ∈ matrixCoefficientSet

The group-like element is a matrix coefficient of the rank-one group-like comodule.

@[simp]

theorem TauCeti.Comodule.groupLike_rankOne_matrixCoefficientSubmodule_eq_span_singleton {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (g : GroupLike R C) : matrixCoefficientSubmodule = R ∙ ↑g

The coefficient set of the rank-one group-like comodule spans exactly the line generated by its group-like element.

theorem TauCeti.Comodule.groupLike_matrixCoefficient_mem_adjoin_singleton {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (g : GroupLike R C) (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m ∈ R[↑g]

A matrix coefficient of a group-like comodule lies in the subalgebra generated by its group-like element.

theorem TauCeti.Comodule.groupLike_matrixCoefficientSubalgebra_le_adjoin_singleton {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (g : GroupLike R C) : matrixCoefficientSubalgebra ≤ R[↑g]

The coefficient algebra of a group-like comodule is contained in the subalgebra generated by its group-like element.

@[simp]

theorem TauCeti.Comodule.groupLike_rankOne_matrixCoefficientSubalgebra_eq_adjoin_singleton {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] (g : GroupLike R C) : matrixCoefficientSubalgebra = R[↑g]

The coefficient algebra of the rank-one group-like comodule is exactly the subalgebra generated by its group-like element.

theorem TauCeti.Comodule.trivial_eq_groupLike_one {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] : trivial = groupLike 1

The trivial comodule is the group-like comodule for the unit group-like element.

theorem TauCeti.Comodule.trivial_matrixCoefficient_mem_span_singleton_one {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m ∈ R ∙ 1

A matrix coefficient of a trivial comodule lies in the line spanned by 1.

theorem TauCeti.Comodule.trivial_matrixCoefficientSubmodule_le_span_singleton_one {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] : matrixCoefficientSubmodule ≤ R ∙ 1

The coefficient submodule of a trivial comodule is contained in the line spanned by 1.

theorem TauCeti.Comodule.trivial_rankOne_matrixCoefficientSubmodule_eq_span_singleton_one {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] : matrixCoefficientSubmodule = R ∙ 1

The coefficient submodule of the rank-one trivial comodule is exactly the line spanned by 1.

theorem TauCeti.Comodule.trivial_matrixCoefficient_mem_bot {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] R) (m : M) : matrixCoefficient φ m ∈ ⊥

A matrix coefficient of a trivial comodule lies in the bottom R-subalgebra.

theorem TauCeti.Comodule.trivial_matrixCoefficientSubalgebra_le_bot {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] : matrixCoefficientSubalgebra ≤ ⊥

The coefficient algebra of a trivial comodule is contained in the bottom subalgebra.

@[simp]

theorem TauCeti.Comodule.trivial_matrixCoefficientSubalgebra_eq_bot {R : Type u} {C : Type v} [CommSemiring R] [Semiring C] [Bialgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] : matrixCoefficientSubalgebra = ⊥

The coefficient algebra of a trivial comodule is the bottom R-subalgebra.