The stabilizer of a subspace of a representation

Let H be a commutative Hopf algebra over a field k and M a right H-comodule, that is, a representation of the affine group G = Spec H. A subspace W ≤ M has a stabilizer: the closed subgroup of G whose points carry W onto itself. In coordinates it is cut out by the matrix coefficients c(ψ ∘ q, w) pairing vectors w ∈ W with functionals vanishing on W (here q : M → M ⧸ W is the quotient map), together with their antipodes.

This file constructs that Hopf ideal and characterizes it in four ways.

• Its points with values in any commutative k-algebra A are the points whose action carries A ⊗ W onto itself.
• It is the smallest Hopf ideal containing the coefficients c(ψ ∘ q, w).
• It is zero, so the stabilizer is all of G, exactly when W is a subcomodule.
• Its Lie algebra consists of the tangent vectors whose differentiated action preserves W.

The last statement is the infinitesimal input to the comparison of G-stable and Lie(G)-stable subspaces.

Main declarations

• Submodule.stabilizerHopfIdeal: the Hopf ideal of the stabilizer of W.
• Submodule.stabilizerHopfIdeal_le_ker_iff: its points are the points carrying A ⊗ W onto itself.
• Submodule.stabilizerHopfIdeal_le_iff: its universal property among Hopf ideals.
• Submodule.stabilizerHopfIdeal_eq_bot_iff: it vanishes exactly when W is a subcomodule.
• Submodule.mem_lieSubalgebra_stabilizerHopfIdeal_iff: its Lie algebra is the stabilizer of W under the differentiated representation.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 4 and 10.
• J. E. Humphreys, Linear Algebraic Groups, §13.

def Submodule.stabilizerHopfIdeal {k : Type u} (H : Type v) {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) : TauCeti.HopfIdeal k H

The Hopf ideal of the stabilizer of a subspace W of a comodule M.

It is generated by the matrix coefficients c(ψ ∘ q, w), for w ∈ W and functionals ψ on M ⧸ W, together with their antipodes. Contravariantly, it cuts out the closed subgroup of Spec H preserving W.

Equations

• Submodule.stabilizerHopfIdeal H W = TauCeti.HopfIdeal.ofSpan (Submodule.stabilizerGenerators✝ H W) ⋯ ⋯ ⋯

theorem Submodule.matrixCoefficient_mem_stabilizerHopfIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) (ψ : Module.Dual k (M ⧸ W)) {w : M} (hw : w ∈ W) : TauCeti.Comodule.matrixCoefficient (ψ ∘ₗ W.mkQ) w ∈ stabilizerHopfIdeal H W

A matrix coefficient pairing a vector of W with a functional vanishing on W lies in the stabilizer Hopf ideal.

theorem Submodule.stabilizerHopfIdeal_le_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) (J : TauCeti.HopfIdeal k H) : stabilizerHopfIdeal H W ≤ J ↔ ∀ (ψ : Module.Dual k (M ⧸ W)), ∀ w ∈ W, TauCeti.Comodule.matrixCoefficient (ψ ∘ₗ W.mkQ) w ∈ J

The stabilizer Hopf ideal is the smallest Hopf ideal containing the matrix coefficients c(ψ ∘ q, w); contravariantly, the stabilizer is the largest closed subgroup on which these coefficients vanish.

theorem Submodule.stabilizerHopfIdeal_eq_bot_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) : stabilizerHopfIdeal H W = ⊥ ↔ ∀ w ∈ W, TauCeti.Comodule.coact w ∈ (TensorProduct.map W.subtype LinearMap.id).range

The stabilizer of W is the whole group exactly when W is a subcomodule: the coaction of every vector of W lies in W ⊗ H.

theorem Submodule.mem_lieSubalgebra_stabilizerHopfIdeal_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) (d : Derivation k H (TauCeti.Bialgebra.CounitAlgebra k H k)) : d ∈ (stabilizerHopfIdeal H W).lieSubalgebra ↔ ∀ w ∈ W, (TauCeti.Comodule.differential d) w ∈ W

The Lie algebra of the stabilizer of W consists of the tangent vectors whose differentiated action preserves W.

theorem Submodule.stabilizerHopfIdeal_le_ker_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] (W : Submodule k M) {A : Type u_1} [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : (stabilizerHopfIdeal H W).toIdeal ≤ RingHom.ker g.ofConv ↔ map (TauCeti.Comodule.endOfPoint M g.ofConv) (baseChange A W) = baseChange A W

An algebra-valued point lies in the stabilizer of W exactly when its action carries the scalar extension of W onto itself.