feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after…

… faithfully flat base change (#20808)

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Algebra.Lie.BaseChange
 import Mathlib.Algebra.Lie.Solvable
 import Mathlib.Algebra.Lie.Quotient
 import Mathlib.Algebra.Lie.Normalizer

Mathlib/Algebra/Lie/Solvable.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Lie.Abelian
+import Mathlib.Algebra.Lie.BaseChange
 import Mathlib.Algebra.Lie.IdealOperations
 import Mathlib.Order.Hom.Basic
+import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
 
 /-!
 # Solvable Lie algebras
@@ -121,6 +123,21 @@ theorem abelian_iff_derived_succ_eq_bot (I : LieIdeal R L) (k : ℕ) :
     IsLieAbelian (derivedSeriesOfIdeal R L k I) ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ := by
   rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]
 
+open TensorProduct in
+@[simp] theorem derivedSeriesOfIdeal_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
+    derivedSeriesOfIdeal A (A ⊗[R] L) k (I.baseChange A) =
+      (derivedSeriesOfIdeal R L k I).baseChange A := by
+  induction k with
+  | zero => simp
+  | succ k ih => simp only [derivedSeriesOfIdeal_succ, ih, ← LieSubmodule.baseChange_top,
+    LieSubmodule.lie_baseChange]
+
+open TensorProduct in
+@[simp] theorem derivedSeries_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
+    derivedSeries A (A ⊗[R] L) k = (derivedSeries R L k).baseChange A := by
+  rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
+    LieSubmodule.baseChange_top]
+
 end LieAlgebra
 
 namespace LieIdeal
@@ -262,6 +279,27 @@ theorem derivedSeries_lt_top_of_solvable [IsSolvable L] [Nontrivial L] :
   rw [LieIdeal.derivedSeries_eq_top n contra] at hn
   exact top_ne_bot hn
 
+open TensorProduct in
+instance {A : Type*} [CommRing A] [Algebra R A] [IsSolvable L] : IsSolvable (A ⊗[R] L) := by
+  obtain ⟨k, hk⟩ := IsSolvable.solvable R L
+  rw [isSolvable_iff A]
+  use k
+  rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]
+
+open TensorProduct in
+variable {A : Type*} [CommRing A] [Algebra R A] [Module.FaithfullyFlat R A] in
+theorem isSolvable_tensorProduct_iff : IsSolvable (A ⊗[R] L) ↔ IsSolvable L := by
+  refine ⟨?_, fun _ ↦ inferInstance⟩
+  rw [isSolvable_iff A, isSolvable_iff R]
+  rintro ⟨k, h⟩
+  use k
+  rw [eq_bot_iff] at h ⊢
+  intro x hx
+  rw [derivedSeries_baseChange] at h
+  specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx
+  rw [LieSubmodule.mem_bot] at h ⊢
+  rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h
+
 end LieAlgebra
 
 variable {R L}

Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

@@ -426,6 +426,22 @@ lemma zero_iff_rTensor_zero [h: FaithfullyFlat R M]
     (by simpa using congr($h (m ⊗ₜ n))), fun h => by
     ext m n; exact (TensorProduct.comm R M N').injective <| (by simpa using congr($h (n ⊗ₜ m)))⟩
 
+/-- If `A` is a faithfully flat `R`-algebra, and `m` is a term of an `R`-module `M`,
+then `1 ⊗ₜ[R] m = 0` if and only if `m = 0`. -/
+@[simp]
+theorem one_tmul_eq_zero_iff {A : Type*} [CommRing A] [Algebra R A] [FaithfullyFlat R A] (m : M) :
+    (1:A) ⊗ₜ[R] m = 0 ↔ m = 0 := by
+  constructor; swap
+  · rintro rfl; rw [tmul_zero]
+  intro h
+  let f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
+  suffices f = 0 by simpa [f] using DFunLike.congr_fun this 1
+  rw [Module.FaithfullyFlat.zero_iff_lTensor_zero R A]
+  ext a
+  apply_fun (a • ·) at h
+  rw [smul_zero, smul_tmul', smul_eq_mul, mul_one] at h
+  simpa [f]
+
 end arbitrary_universe
 
 section fixed_universe