Subgroup-trivial representations and coinvariants

A representation trivial on a closed subgroup has all its matrix coefficients in the subgroup's coinvariant algebra. For a projective underlying module the converse holds as well: linear functionals detect the restricted coaction.

For a normal subgroup, the fixed vectors of a projective representation coincide with those of the scheme-theoretic kernel of the coinvariant projection, under the flatness hypotheses defining that projection. In particular, subgroup-trivial representations are trivial on this kernel. This is the coordinate bridge used to calculate a normal quotient kernel from a representation that detects the subgroup. The subgroup and value algebras may be nonreduced.

The coefficient calculation uses Comodule.comul_matrixCoefficient; detection of point actions uses Comodule.endOfPoint_corestrict and Comodule.endOfPoint_trivial.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• J. E. Humphreys, Linear Algebraic Groups, §11.5.

theorem TauCeti.HopfIdeal.matrixCoefficient_mem_coinvariants_of_quotient_coact_eq_tmul_one {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] (φ : Module.Dual R M) (m : M) (hm : (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1) : Comodule.matrixCoefficient φ m ∈ I.coinvariants

A matrix coefficient of a vector fixed by the restricted subgroup coaction is invariant under right translation by that subgroup. No finiteness or projectivity is required.

theorem TauCeti.HopfIdeal.quotient_coact_eq_tmul_one_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] [Module.Projective R M] (m : M) : (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1 ↔ ∀ (φ : Module.Dual R M), (Ideal.Quotient.mk I.toIdeal) (Comodule.matrixCoefficient φ m) = (algebraMap R (↑H ⧸ I.toIdeal)) (φ m)

The restricted coaction fixes a vector in a projective comodule exactly when all its matrix coefficients restrict to their scalar counit values on the subgroup.

theorem TauCeti.HopfIdeal.matrixCoefficientSubalgebra_le_coinvariants_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] [Module.Projective R M] : Comodule.matrixCoefficientSubalgebra ≤ I.coinvariants ↔ ∀ (m : M), (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1

For a projective comodule, its coefficient algebra lies in the subgroup coinvariants exactly when the subgroup's restricted coaction is trivial.

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.quotient_coact_kernel_coinvariantsι_eq_tmul_one_iff {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] [Module.Projective R M] (hI : I.IsNormal) (m : M) : (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R (CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.coinvariantsι hI)).toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1 ↔ (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1

The vectors fixed by a normal subgroup in a projective comodule are exactly those fixed by the scheme-theoretic kernel of its coinvariant projection. This compares the whole restricted coactions, including infinitesimal information.

theorem TauCeti.HopfIdeal.IsNormal.endOfPoint_eq_id_of_mem_kernel_coinvariantsι {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R (↑H) M] [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] [Module.Projective R M] (hI : I.IsNormal) (hM : ∀ (m : M), (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (hg : g ∈ CommHopfAlgCat.quotientPointsSubgroup H (CommHopfAlgCat.kernelHopfIdeal (CommHopfAlgCat.coinvariantsι hI)) A) : Comodule.endOfPoint M g.ofConv = LinearMap.id

Every point in the scheme-theoretic kernel of a normal coinvariant projection acts trivially on every projective representation trivial on the original subgroup. This holds over arbitrary commutative value algebras.