Matrix coefficients against functionals vanishing on a subspace

Let M be a right comodule over a coalgebra C over a field k, and W ≤ M a subspace. Write q : M → M ⧸ W for the quotient map. The matrix coefficients c(ψ ∘ q, m), for functionals ψ on M ⧸ W, measure how far the coaction moves m out of W.

• The coaction of m lies in W ⊗ C exactly when all these coefficients vanish.
• An algebra-valued point g carries A ⊗ W into itself exactly when g kills these coefficients for every w ∈ W.

These are the coordinate descriptions of subcomodules and of the stabilizer of a subspace.

Main declarations

• Submodule.coact_mem_range_iff_forall_matrixCoefficient_eq_zero: over a field, the coaction of m lies in W ⊗ C exactly when m has no matrix coefficient against a functional vanishing on W.
• Submodule.mapsTo_endOfPoint_baseChange_iff: a point preserves A ⊗ W exactly when it kills those matrix coefficients.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 4.

theorem Submodule.coact_mem_range_iff_forall_matrixCoefficient_eq_zero {k : Type u} {C : Type v} {M : Type w} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [TauCeti.Comodule k C M] (W : Submodule k M) (m : M) : TauCeti.Comodule.coact m ∈ (TensorProduct.map W.subtype LinearMap.id).range ↔ ∀ (ψ : Module.Dual k (M ⧸ W)), TauCeti.Comodule.matrixCoefficient (ψ ∘ₗ W.mkQ) m = 0

Over a field, the coaction of a vector lies in W ⊗ C exactly when every matrix coefficient pairing it with a functional vanishing on W is zero.

theorem Submodule.mapsTo_endOfPoint_baseChange_iff {k : Type u} {C : Type v} {M : Type w} {A : Type u_1} [Field k] [Ring C] [Algebra k C] [Coalgebra k C] [AddCommGroup M] [Module k M] [TauCeti.Comodule k C M] [CommRing A] [Algebra k A] (W : Submodule k M) (g : C →ₐ[k] A) : Set.MapsTo ⇑(TauCeti.Comodule.endOfPoint M g) ↑(baseChange A W) ↑(baseChange A W) ↔ ∀ (ψ : Module.Dual k (M ⧸ W)), ∀ w ∈ W, g (TauCeti.Comodule.matrixCoefficient (ψ ∘ₗ W.mkQ) w) = 0

An algebra-valued point preserves the scalar extension of W exactly when it kills every matrix coefficient pairing a vector of W with a functional vanishing on W.