Joint eigenspaces for normal subgroups

If N is a normal subgroup of G, conjugation by g : G permutes the characters of N. For a representation ρ of G, the operator ρ g carries the joint N-eigenspace of a character χ onto the joint eigenspace of the conjugated character n ↦ χ (g⁻¹ * n * g).

This is the representation-theoretic bridge used in the Lie--Kolchin argument. The derived subgroup supplies characters with nonzero joint weight spaces; normality makes the ambient group permute those characters while transporting their corresponding spaces, and connectedness can then force that permutation to be trivial.

Main declarations

• map_iInf_eigenspace_unitHom_eq_conjNormal: an ambient representation operator maps a normal subgroup's χ-weight space onto the conjugated-character weight space.
• iInf_eigenspace_unitHom_conjNormal_ne_bot_iff: conjugation preserves which character weight spaces are nonzero.
• nonzeroJointWeightAction: the resulting permutation action of the ambient group on the characters having nonzero joint weight space.
• map_iInf_eigenspace_unitHom_eq_self_of_nonzeroJointWeightAction_eq: a character fixed by the permutation action has an ambient-invariant joint weight space.
• map_iInf_eigenspace_unitHom_eq_self_of_mem_ker_nonzeroJointWeightAction: the kernel of that action preserves every nonzero joint weight space.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. E. Humphreys, Linear Algebraic Groups, §17.6.

@[simp]

theorem TauCeti.map_iInf_eigenspace_unitHom_eq_conjNormal {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) (g : G) (χ : ↥N →* Kˣ) : Submodule.map (ρ g) (⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n)) = ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(((MulEquiv.monoidHomCongrLeftEquiv (MulAut.conjNormal g)) χ) n)

Let N be a normal subgroup of G. For a representation ρ of G, the operator ρ g maps the joint N-eigenspace of χ exactly onto the joint eigenspace of the conjugated character n ↦ χ (g⁻¹ * n * g).

No field, finite-dimensionality, commutativity of N, or semisimplicity hypothesis is needed.

theorem TauCeti.iInf_eigenspace_unitHom_conjNormal_ne_bot_iff {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) (g : G) (χ : ↥N →* Kˣ) : ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(((MulEquiv.monoidHomCongrLeftEquiv (MulAut.conjNormal g)) χ) n) ≠ ⊥ ↔ ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥

Conjugating a character by an ambient group element preserves whether its joint weight space for the normal subgroup is nonzero.

def TauCeti.nonzeroJointWeightAction {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) : G →* Equiv.Perm { χ : ↥N →* Kˣ // ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥ }

The ambient group acts by permutations on the characters having nonzero joint weight space for a normal subgroup. This is the abstract permutation action used in the Lie--Kolchin argument.

Equations

• TauCeti.nonzeroJointWeightAction N ρ = { toFun := TauCeti.nonzeroJointWeightEquiv✝ N ρ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.nonzeroJointWeightAction_apply_coe {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) (g : G) (χ : { χ : ↥N →* Kˣ // ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥ }) : ↑(((nonzeroJointWeightAction N ρ) g) χ) = (MulEquiv.monoidHomCongrLeftEquiv (MulAut.conjNormal g)) ↑χ

The underlying character of the permutation action is obtained by conjugating with g.

theorem TauCeti.map_iInf_eigenspace_unitHom_eq_self_of_nonzeroJointWeightAction_eq {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) (g : G) (χ : { χ : ↥N →* Kˣ // ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥ }) (hχ : ((nonzeroJointWeightAction N ρ) g) χ = χ) : Submodule.map (ρ g) (⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(↑χ n)) = ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(↑χ n)

If an ambient group element fixes a nonzero normal-subgroup weight, its representation operator maps the corresponding joint weight space onto itself.

theorem TauCeti.map_iInf_eigenspace_unitHom_eq_self_of_mem_ker_nonzeroJointWeightAction {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [CommRing K] [AddCommGroup V] [Module K V] (N : Subgroup G) [N.Normal] (ρ : G →* Module.End K V) (g : G) (hg : g ∈ (nonzeroJointWeightAction N ρ).ker) (χ : { χ : ↥N →* Kˣ // ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(χ n) ≠ ⊥ }) : Submodule.map (ρ g) (⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(↑χ n)) = ⨅ (n : ↥N), (ρ ↑n).eigenspace ↑(↑χ n)

Every element in the kernel of the permutation action preserves each nonzero normal-subgroup joint weight space.