Extending a nilpotent action by a normalizing element

Let M be a Lie module over L, let H be a Lie subalgebra of L acting nilpotently on M, and let y : L normalize H and act nilpotently on M. This file proves that the Lie subalgebra LieSubalgebra.lieSpan R L (insert y ↑H) spanned by y and H again acts nilpotently on M, so that in particular every element t • y + h acts nilpotently. This is the step by which Hochschild's proof of Ado's theorem enlarges a nilpotently-acting subalgebra one element at a time, and it is applied there to two different modules, so it is stated once for a general module.

Because y normalizes H, that Lie span is already spanned by y and H as a module: its underlying submodule is R ∙ y ⊔ H.toSubmodule. Its elements are therefore exactly the t • y + h with t : R and h ∈ H, which is the form in which the extension lemma is used.

No Noetherian or finiteness hypothesis is needed for the subalgebra statement. Engel's theorem enters only in the variants whose hypothesis on H is the pointwise one, ∀ x ∈ H, IsNilpotent (toEnd x), and those carry [IsNoetherian R M].

Main statements

• LieSubalgebra.lieSpan_insert_toSubmodule: the Lie span of insert y ↑H has underlying submodule R ∙ y ⊔ H.toSubmodule, when y normalizes H.
• LieSubalgebra.lieModule_isNilpotent_lieSpan_insert: the nilpotent-extension lemma. If H acts nilpotently on M and a normalizing element y acts nilpotently on M, then the Lie span of y and H acts nilpotently on M.
• LieSubalgebra.mem_lieSpan_insert_iff: the elements of that Lie span are exactly the t • y + h with h ∈ H, with intro form LieSubalgebra.smul_add_mem_lieSpan_insert.
• LieSubalgebra.lt_lieSpan_insert: that Lie span lies strictly above H when y ∉ H.
• LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert and LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert_of_forall: the pointwise readings, the second one taking the pointwise hypothesis on H as well, together with the t • y + h reading LieSubalgebra.isNilpotent_toEnd_smul_add_of_mem.
• LieIdeal.isNilpotent_toEnd_of_mem_span_singleton_sup: the special case of an ideal, where the normalizing hypothesis is automatic and the conclusion can be read off the submodule R ∙ y ⊔ I.toSubmodule directly, together with its t • y + x reading LieIdeal.isNilpotent_toEnd_smul_add_of_mem.
• Ado.LieAlgebra.isNilpotent_ad_of_mem_span_singleton_sup_nilradical and Ado.LieAlgebra.isNilpotent_ad_smul_add_of_mem_nilradical: the adjoint specialization, that t • y + n is ad-nilpotent for n in the nilradical and y ad-nilpotent.

References

• G. Hochschild, An addition to Ado's theorem, Proc. Amer. Math. Soc. 17 (1966), 531-533.
• [W. Fulton and J. Harris, Representation Theory: A First Course][fulton-harris1991], Appendix E, §E.2.
• Mathlib's LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer in Mathlib/Algebra/Lie/Engel.lean, the source this file follows.

theorem LieSubalgebra.lieSpan_insert_toSubmodule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) : (lieSpan R L (insert y ↑H)).toSubmodule = R ∙ y ⊔ H.toSubmodule

When y normalizes a Lie subalgebra H, the Lie subalgebra generated by H together with y is already spanned by them as a module: its underlying submodule is R ∙ y ⊔ H.toSubmodule.

theorem LieSubalgebra.mem_lieSpan_insert_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) {z : L} : z ∈ lieSpan R L (insert y ↑H) ↔ ∃ (t : R), ∃ h ∈ H, z = t • y + h

When y normalizes a Lie subalgebra H, the elements of the Lie subalgebra spanned by H together with y are exactly the t • y + h with t : R and h ∈ H.

theorem LieSubalgebra.smul_add_mem_lieSpan_insert {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) (t : R) {h : L} (hh : h ∈ H) : t • y + h ∈ lieSpan R L (insert y ↑H)

When y normalizes a Lie subalgebra H, every t • y + h with h ∈ H lies in the Lie subalgebra spanned by H together with y.

theorem LieSubalgebra.lt_lieSpan_insert {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) {y : L} (hy : y ∉ H) : H < lieSpan R L (insert y ↑H)

A Lie subalgebra H lies strictly below the Lie span of H together with an element y ∉ H. No normalizing hypothesis is needed.

theorem LieSubalgebra.lieModule_isNilpotent_lieSpan_insert {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) [LieModule.IsNilpotent (↥H) M] (hyM : IsNilpotent ((LieModule.toEnd R L M) y)) : LieModule.IsNilpotent (↥(lieSpan R L (insert y ↑H))) M

The nilpotent-extension lemma. If a Lie subalgebra H acts nilpotently on M, and an element y normalizing H acts nilpotently on M, then the Lie subalgebra spanned by y and H acts nilpotently on M.

theorem LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) [LieModule.IsNilpotent (↥H) M] (hyM : IsNilpotent ((LieModule.toEnd R L M) y)) {z : L} (hz : z ∈ lieSpan R L (insert y ↑H)) : IsNilpotent ((LieModule.toEnd R L M) z)

Every element of the Lie subalgebra spanned by a normalizing element y and H acts nilpotently on M, as soon as H does and y does.

theorem LieSubalgebra.isNilpotent_toEnd_smul_add_of_mem {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) [LieModule.IsNilpotent (↥H) M] (hyM : IsNilpotent ((LieModule.toEnd R L M) y)) (t : R) {h : L} (hh : h ∈ H) : IsNilpotent ((LieModule.toEnd R L M) (t • y + h))

The t • y + h reading of LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert: if H acts nilpotently on M and a normalizing element y acts nilpotently on M, then so does every t • y + h with h ∈ H.

theorem LieSubalgebra.isNilpotent_toEnd_of_mem_lieSpan_insert_of_forall {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (H : LieSubalgebra R L) {y : L} (hy : y ∈ H.normalizer) (hH : ∀ x ∈ H, IsNilpotent ((LieModule.toEnd R L M) x)) (hyM : IsNilpotent ((LieModule.toEnd R L M) y)) {z : L} (hz : z ∈ lieSpan R L (insert y ↑H)) : IsNilpotent ((LieModule.toEnd R L M) z)

The pointwise form of the nilpotent-extension lemma: if every element of H acts nilpotently on a Noetherian module M, and so does a normalizing element y, then so does every element of the Lie subalgebra spanned by y and H.

theorem LieIdeal.isNilpotent_toEnd_of_mem_span_singleton_sup {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (I : LieIdeal R L) (hI : ∀ x ∈ I, IsNilpotent ((LieModule.toEnd R L M) x)) {y : L} (hy : IsNilpotent ((LieModule.toEnd R L M) y)) {z : L} (hz : z ∈ R ∙ y ⊔ ↑I) : IsNilpotent ((LieModule.toEnd R L M) z)

The nilpotent-extension lemma for an ideal I of L: the normalizing hypothesis is automatic, and the elements covered by the conclusion are exactly those of the submodule R ∙ y ⊔ I.toSubmodule, that is, the elements t • y + x with x ∈ I.

theorem LieIdeal.isNilpotent_toEnd_smul_add_of_mem {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (I : LieIdeal R L) (hI : ∀ x ∈ I, IsNilpotent ((LieModule.toEnd R L M) x)) {y : L} (hy : IsNilpotent ((LieModule.toEnd R L M) y)) (t : R) {x : L} (hx : x ∈ I) : IsNilpotent ((LieModule.toEnd R L M) (t • y + x))

The t • y + x reading of LieIdeal.isNilpotent_toEnd_of_mem_span_singleton_sup: for an ideal I all of whose elements act nilpotently on M, and y acting nilpotently on M, every t • y + x with x ∈ I acts nilpotently on M.

theorem Ado.LieAlgebra.isNilpotent_ad_of_mem_span_singleton_sup_nilradical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] {y : L} (hy : IsNilpotent ((LieAlgebra.ad R L) y)) {z : L} (hz : z ∈ R ∙ y ⊔ ↑(nilradical R L)) : IsNilpotent ((LieAlgebra.ad R L) z)

The adjoint specialization of the nilpotent-extension lemma: if y is ad-nilpotent, then so is every element of R ∙ y ⊔ nilradical R L. Every element of the nilradical is ad-nilpotent, so no nilpotency hypothesis on the ideal is needed.

theorem Ado.LieAlgebra.isNilpotent_ad_smul_add_of_mem_nilradical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] {y : L} (hy : IsNilpotent ((LieAlgebra.ad R L) y)) (t : R) {n : L} (hn : n ∈ nilradical R L) : IsNilpotent ((LieAlgebra.ad R L) (t • y + n))

The t • y + n reading of isNilpotent_ad_of_mem_span_singleton_sup_nilradical: if y is ad-nilpotent, then so is t • y + n for every n in the nilradical.