Solvability, nilpotency and semisimplicity under extension of scalars

Let L be a Lie algebra over a commutative ring R and let A be an R-algebra. Mathlib's LieSubmodule.baseChange extends an ideal I of L to the ideal I.baseChange A of A ⊗[R] L, and LieAlgebra.derivedSeriesOfIdeal_baseChange computes the derived series of an extended ideal by extending the derived series term by term. This file records the same statement for the series L ≥ ⁅I, L⁆ ≥ ⁅I, ⁅I, L⁆⁆ ≥ ⋯ that measures nilpotency of an ideal, and reads both series off as transfer principles:

IsSolvable ↥(I.baseChange A) ↔ IsSolvable ↥I,   IsNilpotent ↥(I.baseChange A) ↔ IsNilpotent ↥I

Ascent — transferring either property from I to I.baseChange A — asks nothing of A. Descent, the → direction of the equivalences as displayed, is exactly where faithful flatness enters, through Submodule.baseChange_inj: a term of either series can vanish after extending scalars only if it vanished already. Applied to the two largest ideals, ascent gives

(radical R L).baseChange A ≤ radical A (A ⊗[R] L),
(nilradical R L).baseChange A ≤ nilradical A (A ⊗[R] L).

Neither containment is forced to be an equality by the transfer principles, because an ideal of A ⊗[R] L need not be extended from L at all, and nothing above bounds the ideals that are not. The case where both sides are ⊥ is the separate statement LieAlgebra.hasTrivialRadical_baseChange_iff: over a field of characteristic zero a finite-dimensional Lie algebra has trivial radical exactly when some field extension of it does, so extending scalars can neither destroy nor create a solvable ideal of a semisimple algebra.

For a finite-dimensional Lie algebra over a field of characteristic zero the containment is an equality: LieAlgebra.radical_baseChange says the radical commutes with a field extension, and LieAlgebra.one_tmul_mem_radical_baseChange_iff reads that as a criterion, so membership in the radical may be tested after extending scalars. The corresponding statement for the nilradical is not proved here and does not follow, since L ⧸ nilradical K L need not have trivial nilradical.

Main results

• LieIdeal.lcs_baseChange: the series ⁅I, ⁅I, … ⁅I, M⁆…⁆⁆ commutes with extension of scalars.
• LieIdeal.isSolvable_baseChange_iff and LieIdeal.isNilpotent_baseChange_iff: an ideal is solvable, respectively nilpotent, exactly when its faithfully flat extension of scalars is.
• LieAlgebra.baseChange_radical_le and LieAlgebra.baseChange_nilradical_le: the extension of the radical, respectively of the nilradical, lands in the radical, respectively the nilradical, of the extended algebra.
• LieAlgebra.hasTrivialRadical_baseChange_iff: in characteristic zero a finite-dimensional Lie algebra has trivial radical exactly when its extension to a field extension does.
• LieAlgebra.radical_baseChange: in characteristic zero the solvable radical of a finite-dimensional Lie algebra commutes with a field extension, with LieAlgebra.one_tmul_mem_radical_baseChange_iff reading it as a membership criterion that may be checked after extending scalars.

References

• [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3][bourbaki1975], Chapter I, §5 and §6, for solvability, nilpotency and the radical under extension of scalars.

@[simp]

theorem LieIdeal.lcs_baseChange {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (k : ℕ) : lcs (LieSubmodule.baseChange A I) (TensorProduct R A M) k = LieSubmodule.baseChange A (I.lcs M k)

The series ⁅I, ⁅I, … ⁅I, M⁆…⁆⁆ commutes with extension of scalars. This is the nilpotency counterpart of Mathlib's LieAlgebra.derivedSeriesOfIdeal_baseChange.

theorem LieIdeal.isSolvable_baseChange {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] (I : LieIdeal R L) [LieAlgebra.IsSolvable ↥I] : LieAlgebra.IsSolvable ↥(LieSubmodule.baseChange A I)

The extension of scalars of a solvable ideal is solvable. No hypothesis on the coefficient algebra is needed in this direction.

theorem LieIdeal.isNilpotent_baseChange {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] (I : LieIdeal R L) [LieRing.IsNilpotent ↥I] : LieRing.IsNilpotent ↥(LieSubmodule.baseChange A I)

The extension of scalars of a nilpotent ideal is nilpotent. No hypothesis on the coefficient algebra is needed in this direction.

@[simp]

theorem LieIdeal.isSolvable_baseChange_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] (I : LieIdeal R L) [Module.FaithfullyFlat R A] : LieAlgebra.IsSolvable ↥(LieSubmodule.baseChange A I) ↔ LieAlgebra.IsSolvable ↥I

An ideal is solvable exactly when its faithfully flat extension of scalars is solvable.

@[simp]

theorem LieIdeal.isNilpotent_baseChange_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] (I : LieIdeal R L) [Module.FaithfullyFlat R A] : LieRing.IsNilpotent ↥(LieSubmodule.baseChange A I) ↔ LieRing.IsNilpotent ↥I

An ideal is nilpotent exactly when its faithfully flat extension of scalars is nilpotent.

theorem LieAlgebra.baseChange_radical_le (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] [IsNoetherian R L] : LieSubmodule.baseChange A (radical R L) ≤ radical A (TensorProduct R A L)

The extension of scalars of the solvable radical lands in the solvable radical. Nothing formal makes the containment an equality, since an ideal of A ⊗[R] L need not be extended from L; over a field of characteristic zero it is one, which is LieAlgebra.radical_baseChange.

theorem LieAlgebra.baseChange_nilradical_le (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type u_3) [CommRing A] [Algebra R A] [IsNoetherian R L] : LieSubmodule.baseChange A (Ado.LieAlgebra.nilradical R L) ≤ Ado.LieAlgebra.nilradical A (TensorProduct R A L)

The extension of scalars of the nilradical lands in the nilradical.

@[simp]

theorem LieAlgebra.hasTrivialRadical_baseChange_iff (K : Type u_1) (L : Type u_2) (A : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Field A] [Algebra K A] : HasTrivialRadical A (TensorProduct K A L) ↔ HasTrivialRadical K L

Triviality of the radical is insensitive to a field extension. In characteristic zero a finite-dimensional Lie algebra has trivial radical exactly when its extension of scalars to a field extension does.

The ← direction is the substantive one: it says that extending scalars cannot create a solvable ideal. Neither direction follows from LieIdeal.isSolvable_baseChange_iff, which only speaks of ideals extended from L. Characteristic zero is a genuine hypothesis here, not a convenience.

@[simp]

theorem LieAlgebra.radical_baseChange (K : Type u_1) (L : Type u_2) (A : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Field A] [Algebra K A] : radical A (TensorProduct K A L) = LieSubmodule.baseChange A (radical K L)

In characteristic zero the solvable radical commutes with a field extension. For a finite-dimensional Lie algebra L over a field K of characteristic zero and a field extension A of K, the radical of A ⊗[K] L is the extension of scalars of the radical of L.

Characteristic zero is a genuine hypothesis, not a convenience. The equality determines the radical of A ⊗[K] L completely, although it says nothing about individual solvable ideals of A ⊗[K] L, which need not themselves be extended from L; as a test for membership in the radical it is LieAlgebra.one_tmul_mem_radical_baseChange_iff.

theorem LieAlgebra.one_tmul_mem_radical_baseChange_iff (K : Type u_1) (L : Type u_2) (A : Type u_3) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [Field A] [Algebra K A] (x : L) : 1 ⊗ₜ[K] x ∈ radical A (TensorProduct K A L) ↔ x ∈ radical K L

Membership in the radical may be checked after a field extension. In characteristic zero a vector of a finite-dimensional Lie algebra lies in the solvable radical exactly when its canonical image in an extension of scalars does.