The stabilizer of a vector in 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 vector v ∈ M has a stabilizer: the closed subgroup of G whose points fix v. In coordinates it is cut out by the equations c(φ, v) = φ(v) for the matrix coefficients of v, with φ running over the functionals on M.

The construction reduces to the stabilizer of a subspace. In M × k, with k the trivial representation, a point fixes v exactly when it carries the line through (v, 1) onto itself, because it cannot rescale the second coordinate. This file takes the stabilizer Hopf ideal of that line and characterizes it intrinsically.

• Its points with values in any commutative k-algebra A are the points fixing 1 ⊗ v in A ⊗ M. Its rational points are those fixing v. Nilpotent values of A are allowed, so this is the scheme-theoretic stabilizer.
• It is the smallest Hopf ideal containing the elements c(φ, v) - φ(v).
• It is zero, so the stabilizer is all of G, exactly when v is a fixed vector.
• Its Lie algebra consists of the tangent vectors whose differentiated action kills v.
• Over a field of characteristic zero it is smooth, by Cartier's theorem, so its dimension is the dimension of that Lie algebra. Equivalently, the dimension of the group is the dimension of the stabilizer plus the dimension of the space 𝔤 • v of images of v under the Lie algebra 𝔤. Geometrically, 𝔤 • v is the tangent space at v to the orbit of v, so this is the infinitesimal form of dim G = dim Stab_G(v) + dim (G • v).

Applied to the adjoint representation, these statements say that the Lie algebra of the centralizer of an element x of the Lie algebra is the kernel of ad x, and in characteristic zero that the centralizer has dimension dim ker (ad x).

Main declarations

• TauCeti.Comodule.stabilizerHopfIdeal: the Hopf ideal of the stabilizer of a vector.
• TauCeti.Comodule.stabilizerHopfIdeal_le_ker_iff: its points are the points fixing 1 ⊗ v.
• TauCeti.Comodule.mem_quotientPointsSubgroup_stabilizerHopfIdeal_iff: its rational points are the rational points fixing v.
• TauCeti.Comodule.matrixCoefficient_sub_algebraMap_mem_stabilizerHopfIdeal and TauCeti.Comodule.stabilizerHopfIdeal_le_iff: its defining equations, and its universal property among Hopf ideals.
• TauCeti.Comodule.basePointsRepresentation_prodTrivial: rational points act on M × k through M, fixing the trivial coordinate.
• TauCeti.Comodule.stabilizerHopfIdeal_basePointsRepresentation: acting on the vector conjugates its scheme-theoretic stabilizer.
• TauCeti.Comodule.stabilizerHopfIdeal_eq_bot_iff: it vanishes exactly when v is fixed.
• TauCeti.Comodule.mem_lieSubalgebra_stabilizerHopfIdeal_iff and TauCeti.Comodule.lieSubalgebra_stabilizerHopfIdeal: its Lie algebra is the annihilator of v under the differentiated representation.
• TauCeti.Comodule.ringKrullDim_quotient_stabilizerHopfIdeal and TauCeti.Comodule.ringKrullDim_quotient_stabilizerHopfIdeal_add_finrank_range: in characteristic zero, the stabilizer has the dimension of its Lie algebra, and together with 𝔤 • v it accounts for the dimension of the group.

References

• J. S. Milne, Algebraic Groups (2017), §1.c and Chapter 10.
• J. E. Humphreys, Linear Algebraic Groups, §13.

@[implicit_reducible]

def TauCeti.Comodule.prodTrivial (k : Type u) (H : Type v) {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] : Comodule k H (M × k)

The product M × k of a comodule with the trivial comodule k. The stabilizer of a vector v is the stabilizer of the line through (v, 1) in this comodule, and the orbit of v is realized as the projective orbit of that line. Install it with attribute [local instance] TauCeti.Comodule.prodTrivial.

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

The Hopf ideal of the stabilizer of a vector v of a comodule M.

It is the stabilizer Hopf ideal of the line through (v, 1) in M × k, where k carries the trivial coaction. Contravariantly, it cuts out the closed subgroup of Spec H fixing v.

theorem TauCeti.Comodule.stabilizerHopfIdeal_def (k : Type u) (H : Type v) {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) : stabilizerHopfIdeal k H v = Submodule.stabilizerHopfIdeal H (k ∙ (v, 1))

The stabilizer of v is the stabilizer of the line through (v, 1) in M × k.

theorem TauCeti.Comodule.matrixCoefficient_prodTrivial {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (Φ : M × k →ₗ[k] k) (v : M) : matrixCoefficient Φ (v, 1) = matrixCoefficient (Φ ∘ₗ LinearMap.inl k M k) v + (algebraMap k H) (Φ (0, 1))

A matrix coefficient of (v, 1) in M × k is a matrix coefficient of v plus a constant.

@[simp]

theorem TauCeti.Comodule.basePointsRepresentation_prodTrivial {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (g : WithConv (H →ₐ[k] k)) (v : M) (c : k) : ((basePointsRepresentation (M × k)) g) (v, c) = (((basePointsRepresentation M) g) v, c)

A rational point acts on M × k through its action on M, fixing the trivial coordinate.

theorem TauCeti.Comodule.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] [Comodule k H M] (v : M) {A : Type u_1} [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : (stabilizerHopfIdeal k H v).toIdeal ≤ RingHom.ker g.ofConv ↔ (endOfPoint M g.ofConv) (1 ⊗ₜ[k] v) = 1 ⊗ₜ[k] v

An algebra-valued point lies in the stabilizer of v exactly when it fixes 1 ⊗ v.

theorem TauCeti.Comodule.mem_quotientPointsSubgroup_stabilizerHopfIdeal_iff_endOfPoint {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) {A : Type u_1} [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (stabilizerHopfIdeal k H v) ↧A ↔ (endOfPoint M g.ofConv) (1 ⊗ₜ[k] v) = 1 ⊗ₜ[k] v

An algebra-valued point lies in the stabilizer precisely when it fixes the constant extension of the vector. The value algebra may be nonreduced.

theorem TauCeti.Comodule.mem_quotientPointsSubgroup_stabilizerHopfIdeal_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) (g : WithConv (H →ₐ[k] k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (stabilizerHopfIdeal k H v) ↧k ↔ ((basePointsRepresentation M) g) v = v

A rational point lies in the stabilizer of v exactly when it fixes v.

theorem TauCeti.Comodule.stabilizerHopfIdeal_le_iff {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) (J : HopfIdeal k H) : stabilizerHopfIdeal k H v ≤ J ↔ ∀ (φ : Module.Dual k M), matrixCoefficient φ v - (algebraMap k H) (φ v) ∈ J

The stabilizer Hopf ideal of v is the smallest Hopf ideal containing the elements c(φ, v) - φ(v); contravariantly, the stabilizer is the largest closed subgroup on which the matrix coefficients of v take their values at the identity.

theorem TauCeti.Comodule.matrixCoefficient_sub_algebraMap_mem_stabilizerHopfIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) (φ : Module.Dual k M) : matrixCoefficient φ v - (algebraMap k H) (φ v) ∈ stabilizerHopfIdeal k H v

The elements c(φ, v) - φ(v) lie in the stabilizer Hopf ideal of v.

theorem TauCeti.Comodule.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] [Comodule k H M] (v : M) : stabilizerHopfIdeal k H v = ⊥ ↔ coact v = v ⊗ₜ[k] 1

The stabilizer of v is the whole group exactly when v is a fixed vector.

@[simp]

theorem TauCeti.Comodule.stabilizerHopfIdeal_zero {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] : stabilizerHopfIdeal k H 0 = ⊥

The stabilizer of 0 is the whole group.

theorem TauCeti.Comodule.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] [Comodule k H M] (v : M) (d : Derivation k H (Bialgebra.CounitAlgebra k H k)) : d ∈ (stabilizerHopfIdeal k H v).lieSubalgebra ↔ (differential d) v = 0

The Lie algebra of the stabilizer of v consists of the tangent vectors whose differentiated action kills v.

theorem TauCeti.Comodule.stabilizerHopfIdeal_basePointsRepresentation {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) (g : WithConv (H →ₐ[k] k)) : stabilizerHopfIdeal k H (((basePointsRepresentation M) g) v) = (stabilizerHopfIdeal k H v).conjugate g

Acting on a vector by a rational point conjugates its scheme-theoretic stabilizer. This is an equality of defining Hopf ideals, including their equations on nonreduced coefficient algebras.

theorem TauCeti.Comodule.lieSubalgebra_stabilizerHopfIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] (v : M) : (stabilizerHopfIdeal k H v).lieSubalgebra.toSubmodule = ((↑differential).flip v).ker

The Lie algebra of a stabilizer. The Lie algebra of the stabilizer of v is the kernel of the linear map d ↦ d • v given by the differentiated representation.

theorem TauCeti.Comodule.ringKrullDim_quotient_stabilizerHopfIdeal {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [CharZero k] [Algebra.FiniteType k H] (v : M) : ringKrullDim (H ⧸ (stabilizerHopfIdeal k H v).toIdeal) = ↑(Module.finrank k ↥((↑differential).flip v).ker)

The dimension of a stabilizer. Over a field of characteristic zero, the stabilizer of v in a finite-type affine group has the dimension of the space of tangent vectors killing v.

theorem TauCeti.Comodule.ringKrullDim_quotient_stabilizerHopfIdeal_add_finrank_range {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [CharZero k] [Algebra.FiniteType k H] (v : M) : ringKrullDim (H ⧸ (stabilizerHopfIdeal k H v).toIdeal) + ↑(Module.finrank k ↥((↑differential).flip v).range) = ringKrullDim H

Dimension of a stabilizer and of an orbit tangent space. Over a field of characteristic zero, the dimension of a finite-type affine group is the dimension of the stabilizer of v plus the dimension of the space 𝔤 • v swept out by the differentiated representation.