Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.Normal.SubgroupWeights

Weight spaces of a closed subgroup in a representation #

Let H be the coordinate Hopf algebra of an affine group G, let the Hopf ideal I cut out a closed subgroup N, and let V be a representation of G. A character of N is a group-like element χ of H ⧸ I, and the χ-weight space of V consists of the vectors on which N acts through χ: those whose coaction, restricted to N, is v ↦ v ⊗ χ. Characters and weight spaces are scheme-theoretic, so nonreduced subgroups such as μ_p are allowed.

A rational point g of G normalizing N restricts to an automorphism of N, whose coordinate map is a bialgebra endomorphism of H ⧸ I. Acting by g carries the χ-weight space into the weight space of the character n ↦ χ (g⁻¹ n g). Every rational point normalizes a normal subgroup, so the sum of the weight spaces of a normal subgroup is stable under all rational points. Over an algebraically closed field and for reduced H of finite type, rational points detect subcomodules, so this sum is a subrepresentation of V; over a field the sum is direct.

This is the first step of the classical proof that a normal subgroup is the kernel of a representation: by Chevalley's theorem N is the stabilizer of a line, which lies in one weight space of N, and G acts on the block-diagonal endomorphisms of the sum of the weight spaces with kernel N.

Main declarations #

References #

source
noncomputable def TauCeti.HopfIdeal.weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (V : Type w) [AddCommMonoid V] [Module R V] [Comodule R H V] (χ : GroupLike R (H ⧸ I.toIdeal)) :
Submodule R V

The weight space of a character χ of the closed subgroup N cut out by I in a representation V of the ambient group: the vectors on which N acts through χ. In coordinates, χ is a group-like element of H ⧸ I, and the coaction of V, restricted to N, sends a weight vector v to v ⊗ χ.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.HopfIdeal.mem_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] {χ : GroupLike R (H ⧸ I.toIdeal)} {v : V} :
    v ∈ I.weightSpace V χ ↔ (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ R I.toIdeal).toLinearMap) (Comodule.coact v) = v ⊗ₜ[R] ↑χ

    Membership in a weight space of a closed subgroup, in terms of the coaction of the ambient group: restricting the coefficients to the subgroup gives v ⊗ χ.

    source
    theorem TauCeti.HopfIdeal.mem_weightSpace_iff_endOfPoint {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] (χ : GroupLike R (H ⧸ I.toIdeal)) (v : V) :
    v ∈ I.weightSpace V χ ↔ (Comodule.endOfPoint V (Ideal.Quotient.mkₐ R I.toIdeal)) (1 ⊗ₜ[R] v) = ↑χ ⊗ₜ[R] v

    A weight vector of a closed subgroup is detected by the universal point of the subgroup, the quotient map H → H ⧸ I, even over a nonreduced base ring.

    source
    theorem TauCeti.HopfIdeal.endOfPoint_comp_mkₐ_tmul_of_mem_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] {A : Type u_1} [CommSemiring A] [Algebra R A] (f : H ⧸ I.toIdeal →ₐ[R] A) (a : A) {χ : GroupLike R (H ⧸ I.toIdeal)} {v : V} (hv : v ∈ I.weightSpace V χ) :
    (Comodule.endOfPoint V (f.comp (Ideal.Quotient.mkₐ R I.toIdeal))) (a ⊗ₜ[R] v) = (a * f ↑χ) ⊗ₜ[R] v

    A point of the closed subgroup acts on the χ-weight space by its value on χ.

    source
    theorem TauCeti.HopfIdeal.basePointsRepresentation_mem_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] (g : WithConv (H →ₐ[R] R)) (hg : I ≤ I.conjugate g⁻¹) {χ : GroupLike R (H ⧸ I.toIdeal)} {v : V} (hv : v ∈ I.weightSpace V χ) :
    ((Comodule.basePointsRepresentation V) g) v ∈ I.weightSpace V ((GroupLike.map (I.quotientPointConjugation g⁻¹ hg)) χ)

    Normalizing points permute weight spaces. If a rational point g normalizes the closed subgroup N cut out by I, then acting by g carries the χ-weight space of N into the weight space of the conjugate character n ↦ χ (g⁻¹ n g).

    source
    theorem TauCeti.HopfIdeal.IsNormal.basePointsRepresentation_mem_iSup_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] (hI : I.IsNormal) (g : WithConv (H →ₐ[R] R)) {v : V} (hv : v ∈ ⨆ (χ : GroupLike R (H ⧸ I.toIdeal)), I.weightSpace V χ) :
    ((Comodule.basePointsRepresentation V) g) v ∈ ⨆ (χ : GroupLike R (H ⧸ I.toIdeal)), I.weightSpace V χ

    The weight spaces of a normal closed subgroup are permuted by every rational point, so their sum is stable under the action of rational points.

    source
    theorem TauCeti.HopfIdeal.IsNormal.map_basePointsRepresentation_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] (hI : I.IsNormal) (g : WithConv (H →ₐ[R] R)) (χ : GroupLike R (H ⧸ I.toIdeal)) :
    Submodule.map ((Comodule.basePointsRepresentation V) g) (I.weightSpace V χ) = I.weightSpace V ((GroupLike.map (I.quotientPointConjugation g⁻¹ ⋯)) χ)

    Rational points permute the weight spaces of a normal subgroup. A rational point g maps the χ-weight space of a normal closed subgroup N onto the weight space of the conjugate character n ↦ χ (g⁻¹ n g).

    source
    @[simp]
    theorem TauCeti.HopfIdeal.weightSpace_subcomodule {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {V : Type w} [AddCommMonoid V] [Module R V] [Comodule R H V] [Module.Flat R H] (I : HopfIdeal R H) [Module.Flat R (H ⧸ I.toIdeal)] (W : Subcomodule R H V) (χ : GroupLike R (H ⧸ I.toIdeal)) :
    I.weightSpace (↥W) χ = Submodule.comap (SMulMemClass.subtype W) (I.weightSpace V χ)

    The weight space of a closed subgroup in a subrepresentation is the preimage of its weight space in the ambient representation, when the coordinate algebras of the group and subgroup are flat over the base.

    source
    theorem TauCeti.HopfIdeal.iSupIndep_weightSpace {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (I : HopfIdeal k H) (V : Type w) [AddCommGroup V] [Module k V] [Comodule k H V] :
    iSupIndep (I.weightSpace V)

    Over a field, the weight spaces of a closed subgroup belonging to distinct characters are independent.

    source
    noncomputable def TauCeti.HopfIdeal.IsNormal.iSupWeightSpaceSubcomodule {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (V : Type w) [AddCommGroup V] [Module k V] [Comodule k H V] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] {I : HopfIdeal k H} (hI : I.IsNormal) :
    Subcomodule k H V

    The weight spaces of a normal subgroup span a subrepresentation. For a normal closed subgroup N of a reduced affine group of finite type over an algebraically closed field, the sum of the weight spaces of N in a representation V is a subcomodule of V.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.HopfIdeal.IsNormal.iSupWeightSpaceSubcomodule_toSubmodule {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (V : Type w) [AddCommGroup V] [Module k V] [Comodule k H V] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] {I : HopfIdeal k H} (hI : I.IsNormal) :
      (iSupWeightSpaceSubcomodule V hI).toSubmodule = ⨆ (χ : GroupLike k (H ⧸ I.toIdeal)), I.weightSpace V χ

      The subrepresentation spanned by the weight spaces of a normal subgroup has the expected underlying subspace.

      source
      @[simp]
      theorem TauCeti.HopfIdeal.IsNormal.iSup_weightSpace_iSupWeightSpaceSubcomodule_eq_top {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (V : Type w) [AddCommGroup V] [Module k V] [Comodule k H V] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] {I : HopfIdeal k H} (hI : I.IsNormal) :
      ⨆ (χ : GroupLike k (H ⧸ I.toIdeal)), I.weightSpace (↥(iSupWeightSpaceSubcomodule V hI)) χ = ⊤

      The weight-sum subrepresentation is spanned by its own subgroup weight spaces.