Matrix coefficients as regular-comodule morphisms

For a right comodule M over a coalgebra C, every linear functional φ : M →ₗ[R] R defines a matrix-coefficient map

m ↦ c(φ, m) : M → C.

The comultiplication formula for matrix coefficients says precisely that this is a morphism from M to the regular right comodule C. Applying the counit recovers φ, so whenever the linear dual separates vectors, these morphisms do too. For a free module, they continue to separate vectors after extending scalars to any commutative algebra.

For a finite free comodule, every coefficient morphism lands in the finite coefficient subcoalgebra, viewed as a regular subcomodule. Conversely, the ranges of all coefficient morphisms generate that regular subcomodule. This supplies an intended downstream naturality bridge for Tannakian reconstruction: for each finite comodule, naturality along these corestricted maps compares its component with components on finite regular subcomodules, and joint separation then recovers the original finite-comodule component.

Main declarations

• TauCeti.Comodule.matrixCoefficientHom: a matrix coefficient as a comodule morphism to the regular comodule.
• TauCeti.Comodule.matrixCoefficientHomLinear: linearity in the functional.
• TauCeti.Comodule.counit_baseChange_matrixCoefficientHom: counit evaluation after scalar extension recovers the original functional.
• TauCeti.Comodule.eq_of_matrixCoefficientHom_eq: coefficient morphisms jointly separate vectors in a free module.
• TauCeti.Comodule.eq_of_baseChange_matrixCoefficientHom_eq: joint separation after scalar extension.
• TauCeti.Comodule.matrixCoefficientSubcoalgebraHom: corestriction to the finite coefficient subcoalgebra.
• TauCeti.Comodule.iSup_range_matrixCoefficientHom_eq: the ranges of the coefficient morphisms generate the coefficient subcoalgebra as a regular subcomodule.

References

• M. Sweedler, Hopf Algebras, Chapter 2.
• J. S. Milne, Algebraic Groups (2017), §9.4.

def TauCeti.Comodule.matrixCoefficientHom {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.Dual R M) : Hom R C M C

The matrix-coefficient map attached to a functional, as a morphism from the given comodule to the regular right comodule.

Equations

• TauCeti.Comodule.matrixCoefficientHom φ = { toLinearMap := TauCeti.Comodule.matrixCoefficientLinear φ, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHom_toLinearMap {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.Dual R M) : (matrixCoefficientHom φ).toLinearMap = matrixCoefficientLinear φ

The underlying linear map of a matrix-coefficient morphism is the corresponding matrix-coefficient linear map.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHom_apply {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.Dual R M) (m : M) : (matrixCoefficientHom φ) m = matrixCoefficient φ m

Evaluating a matrix-coefficient morphism gives the corresponding matrix coefficient.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHom_zero {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] : matrixCoefficientHom 0 = 0

The zero functional gives the zero matrix-coefficient morphism.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHom_add {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.Dual R M) : matrixCoefficientHom (φ + ψ) = matrixCoefficientHom φ + matrixCoefficientHom ψ

Matrix-coefficient morphisms are additive in the functional.

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHom_smul {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] (r : R) (φ : Module.Dual R M) : matrixCoefficientHom (r • φ) = r • matrixCoefficientHom φ

Matrix-coefficient morphisms commute with scalar multiplication of the functional.

def TauCeti.Comodule.matrixCoefficientHomLinear {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.Dual R M →ₗ[R] Hom R C M C

Matrix-coefficient morphisms depend linearly on the functional.

Equations

• TauCeti.Comodule.matrixCoefficientHomLinear = { toFun := TauCeti.Comodule.matrixCoefficientHom, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Comodule.matrixCoefficientHomLinear_apply {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.Dual R M) : matrixCoefficientHomLinear φ = matrixCoefficientHom φ

Applying the linear family of matrix-coefficient morphisms gives the morphism attached to that functional.

theorem TauCeti.Comodule.eq_of_matrixCoefficientHom_eq_of_dual_eval_injective {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] {m n : M} (h : ∀ (φ : Module.Dual R M), (matrixCoefficientHom φ) m = (matrixCoefficientHom φ) n) (hdual : Function.Injective ⇑(Module.Dual.eval R M)) : m = n

Matrix-coefficient morphisms jointly separate vectors whenever the linear dual does.

theorem TauCeti.Comodule.eq_of_matrixCoefficientHom_eq {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] {m n : M} (h : ∀ (φ : Module.Dual R M), (matrixCoefficientHom φ) m = (matrixCoefficientHom φ) n) : m = n

For a free module, matrix-coefficient morphisms to the regular comodule jointly separate vectors.

theorem TauCeti.Comodule.counit_baseChange_matrixCoefficientHom {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] (A : Type x) [CommSemiring A] [Algebra R A] (φ : Module.Dual R M) (z : TensorProduct R A M) : (TensorProduct.AlgebraTensorModule.rid R A A) ((LinearMap.baseChange A CoalgebraStruct.counit) ((LinearMap.baseChange A (matrixCoefficientHom φ).toLinearMap) z)) = ((Module.Dual.baseChange A) φ) z

Applying the scalar-extended counit after a scalar-extended matrix-coefficient morphism recovers the scalar extension of the original functional.

theorem TauCeti.Comodule.eq_of_baseChange_matrixCoefficientHom_eq {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] (A : Type x) [CommSemiring A] [Algebra R A] [Module.Free R M] {x y : TensorProduct R A M} (h : ∀ (φ : Module.Dual R M), (LinearMap.baseChange A (matrixCoefficientHom φ).toLinearMap) x = (LinearMap.baseChange A (matrixCoefficientHom φ).toLinearMap) y) : x = y

After extending scalars to a commutative algebra, the base changes of all matrix-coefficient morphisms still jointly separate vectors.

noncomputable def TauCeti.Comodule.matrixCoefficientSubcoalgebraHom {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.Flat R C] (φ : Module.Dual R M) : Hom R C M ↥matrixCoefficientSubcoalgebra.toRegularSubcomodule

A matrix-coefficient morphism corestricted to the coefficient subcoalgebra, viewed as a finite regular subcomodule.

Equations

• TauCeti.Comodule.matrixCoefficientSubcoalgebraHom φ = (TauCeti.Comodule.matrixCoefficientHom φ).codRestrict TauCeti.Comodule.matrixCoefficientSubcoalgebra.toRegularSubcomodule ⋯

@[simp]

theorem TauCeti.Comodule.matrixCoefficientSubcoalgebraHom_apply_coe {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.Flat R C] (φ : Module.Dual R M) (m : M) : ↑((matrixCoefficientSubcoalgebraHom φ) m) = (matrixCoefficientHom φ) m

Including a corestricted coefficient morphism into the ambient regular comodule recovers the original matrix-coefficient morphism.

theorem TauCeti.Comodule.range_matrixCoefficientHom_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] (φ : Module.Dual R M) : (matrixCoefficientHom φ).range ≤ matrixCoefficientSubcoalgebra.toRegularSubcomodule

The range of every matrix-coefficient morphism lies in the coefficient subcoalgebra viewed as a regular subcomodule.

@[simp]

theorem TauCeti.Comodule.iSup_range_matrixCoefficientHom_eq {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), (matrixCoefficientHom φ).range = matrixCoefficientSubcoalgebra.toRegularSubcomodule

The coefficient subcoalgebra, viewed as a regular subcomodule, is generated by the ranges of all matrix-coefficient morphisms.