Extending nilrepresentations across split ideal extensions

Let ψ : H →ₗ⁅K⁆ LieDerivation K S S define a split extension S ⋊⁅ψ⁆ H of Lie algebras over a field, with S finite-dimensional, and let σ be a finite-dimensional representation of S. This file extends σ to a finite-dimensional representation ρ of S ⋊⁅ψ⁆ H that keeps control of the kernel and of nilpotence on S:

• every element of S killed by ρ is killed by σ;
• an element of S acts nilpotently under ρ exactly when it does under σ.

The construction works whenever every derivation ψ h takes values in a Lie ideal N of S that acts nilpotently under σ. The kernel I of the enveloping-algebra extension of σ is a cofinite two-sided ideal of U(S), and a power of I ⊔ N.envelopingIdeal refines it to a cofinite ideal J stable under the lifted derivations. The representation is then the multiplication-plus-derivation action of S ⋊⁅ψ⁆ H on U(S) ⧸ J.

Two choices of N give the two cases of Fulton–Harris, Proposition E.5:

• in characteristic zero, every derivation of a solvable S takes values in its nilradical, so a nilrepresentation of S extends; the extension is again a nilrepresentation when the nilradical of S ⋊⁅ψ⁆ H lies in that of S;
• in any characteristic, when S ⋊⁅ψ⁆ H is nilpotent, a representation of S by nilpotent operators extends to one of S ⋊⁅ψ⁆ H by nilpotent operators.

Iterating these extensions along a flag of ideals is how a faithful nilrepresentation of the centre grows into a representation of the whole Lie algebra in the proof of Ado's theorem.

Main results

• Ado.exists_semiDirectSum_rep_of_forall_mem: the extension for derivations with values in a Lie ideal acting nilpotently.
• Ado.exists_semiDirectSum_rep_of_isSolvable: in characteristic zero, a nilrepresentation of a solvable ideal extends, and the extension is a nilrepresentation when the nilradical of the extension lies in that of the ideal.
• Ado.exists_semiDirectSum_rep_of_isNilpotent: on a nilpotent split extension, a representation by nilpotent operators extends to one by nilpotent operators.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, Proposition E.5.
• S. Asgarli, Ado's Theorem, Proposition 2.

theorem Ado.exists_semiDirectSum_rep_of_forall_mem {K : Type u} {S : Type v} {H : Type w} {V : Type x} [Field K] [LieRing S] [LieAlgebra K S] [FiniteDimensional K S] [LieRing H] [LieAlgebra K H] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (ψ : H →ₗ⁅K⁆ LieDerivation K S S) (N : LieIdeal K S) (σ : S →ₗ⁅K⁆ Module.End K V) (hσ : ∀ s ∈ N, IsNilpotent (σ s)) (hψ : ∀ (h : H) (s : S), (ψ h) s ∈ N) : ∃ (W : Type (max u v)) (x : AddCommGroup W) (x_1 : Module K W) (_ : FiniteDimensional K W) (ρ : S ⋊⁅ψ⁆ H →ₗ⁅K⁆ Module.End K W), (ρ.comp (LieAlgebra.SemiDirectSum.inl ψ)).ker ≤ σ.ker ∧ (∀ (s : S), IsNilpotent (ρ ((LieAlgebra.SemiDirectSum.inl ψ) s)) ↔ IsNilpotent (σ s)) ∧ ((∀ (s : S), IsNilpotent (σ s)) → ∀ (y : S ⋊⁅ψ⁆ H), (∀ (s : S), ∃ (n : ℕ), (↑(ψ y.right) ^ n) s = 0) → IsNilpotent (ρ y))

A finite-dimensional representation σ of S extends to a finite-dimensional representation ρ of the split extension S ⋊⁅ψ⁆ H, provided every derivation ψ h takes values in a Lie ideal N of S whose elements act nilpotently under σ. The extension detects every direction of S that σ detects, an element of S acts nilpotently under ρ exactly when it does under σ, and when all of S acts nilpotently under σ, every element whose derivation is locally nilpotent acts nilpotently under ρ.

theorem Ado.exists_semiDirectSum_rep_of_isSolvable {K : Type u} {S : Type v} {H : Type w} {V : Type x} [Field K] [LieRing S] [LieAlgebra K S] [FiniteDimensional K S] [LieRing H] [LieAlgebra K H] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (ψ : H →ₗ⁅K⁆ LieDerivation K S S) [CharZero K] [LieAlgebra.IsSolvable S] (σ : S →ₗ⁅K⁆ Module.End K V) (hσ : ∀ s ∈ LieAlgebra.nilradical K S, IsNilpotent (σ s)) (hnr : ↑(LieAlgebra.nilradical K (S ⋊⁅ψ⁆ H)) ≤ Submodule.map ↑(LieAlgebra.SemiDirectSum.inl ψ) ↑(LieAlgebra.nilradical K S)) : ∃ (W : Type (max u v)) (x : AddCommGroup W) (x_1 : Module K W) (_ : FiniteDimensional K W) (ρ : S ⋊⁅ψ⁆ H →ₗ⁅K⁆ Module.End K W), (ρ.comp (LieAlgebra.SemiDirectSum.inl ψ)).ker ≤ σ.ker ∧ ∀ y ∈ LieAlgebra.nilradical K (S ⋊⁅ψ⁆ H), IsNilpotent (ρ y)

Extension of nilrepresentations across a split solvable ideal. In characteristic zero, a finite-dimensional representation of a solvable S on which the nilradical acts nilpotently extends to a finite-dimensional representation ρ of S ⋊⁅ψ⁆ H that detects every direction of S detected by σ. When the nilradical of S ⋊⁅ψ⁆ H lies in the image of the nilradical of S, the extension is again a nilrepresentation.

theorem Ado.exists_semiDirectSum_rep_of_isNilpotent {K : Type u} {S : Type v} {H : Type w} {V : Type x} [Field K] [LieRing S] [LieAlgebra K S] [FiniteDimensional K S] [LieRing H] [LieAlgebra K H] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (ψ : H →ₗ⁅K⁆ LieDerivation K S S) [LieRing.IsNilpotent (S ⋊⁅ψ⁆ H)] (σ : S →ₗ⁅K⁆ Module.End K V) (hσ : ∀ (s : S), IsNilpotent (σ s)) : ∃ (W : Type (max u v)) (x : AddCommGroup W) (x_1 : Module K W) (_ : FiniteDimensional K W) (ρ : S ⋊⁅ψ⁆ H →ₗ⁅K⁆ Module.End K W), (ρ.comp (LieAlgebra.SemiDirectSum.inl ψ)).ker ≤ σ.ker ∧ ∀ (y : S ⋊⁅ψ⁆ H), IsNilpotent (ρ y)

Extension of nilpotent representations across a nilpotent split extension. Over any field, if S ⋊⁅ψ⁆ H is nilpotent, a finite-dimensional representation of S by nilpotent operators extends to a finite-dimensional representation of S ⋊⁅ψ⁆ H by nilpotent operators that detects every direction of S detected by σ.