feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542)

Generalise `LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed` to any integral domain of characteristic zero.

Co-authored-by: Janos Wolosz <janos.wolosz@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

Author: 3 people

Mathlib/Algebra/Lie/CartanCriterion.lean

@@ -12,6 +12,7 @@ public import Mathlib.LinearAlgebra.Eigenspace.Matrix
 public import Mathlib.LinearAlgebra.Eigenspace.Minpoly
 public import Mathlib.LinearAlgebra.Eigenspace.Semisimple
 public import Mathlib.LinearAlgebra.Lagrange
+public import Mathlib.RingTheory.Flat.Localization
 
 /-!
 # Cartan's criteria
@@ -22,9 +23,9 @@ criterion.
 
 ## Main results
 
-* `LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed`: over an algebraically
-  closed field of characteristic zero, if a finite-dimensional representation `M` of `L` has
-  trivial trace form, then `M` is nilpotent as a `⁅L, L⁆`-module.
+* `LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero`: over a field of characteristic zero,
+  if a finite-dimensional representation `M` of `L` has trivial trace form, then `M` is nilpotent
+  as a `⁅L, L⁆`-module.
 
 ## TODO
 
@@ -37,17 +38,19 @@ criterion.
 * [J. Humphreys, *Introduction to Lie Algebras and ...*](humphreys1972) Chapter II 4.3
 -/
 
-
 namespace LieModule
 
-variable {K L M : Type*}
-  [Field K] [CharZero K] [IsAlgClosed K]
+variable {R K L M : Type*}
+  [Field K] [CharZero K]
   [LieRing L] [LieAlgebra K L]
   [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
+  [CommRing R] [CharZero R] [IsDomain R]
+  [LieAlgebra R L] [Module R M] [LieModule R L M] [IsNoetherian R M] [Module.Free R M]
 
 local notation "φ" => toEnd K L M
 
-open Algebra LieAlgebra LinearMap Module Module.End Polynomial
+open Algebra Function LieAlgebra LinearMap Module Module.End Polynomial
+open scoped TensorProduct
 
 lemma exists_polynomial_eval_sub_aux
     {ι R K : Type*} [Finite ι] [CommRing R] [Field K] [Algebra R K]
@@ -63,8 +66,10 @@ lemma exists_polynomial_eval_sub_aux
   have heq : (⟨a i, ha i⟩ - ⟨a j, ha j⟩ : E) = ⟨a k, ha k⟩ - ⟨a l, ha l⟩ := Subtype.ext hij
   rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]
 
-/-- If the trace form of `M` is zero, then the `⁅L, L⁆`-module `M` is nilpotent. -/
-public theorem isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (h : traceForm K L M = 0) :
+/-- An auxiliary lemma used to prove `LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero`
+which proves the same result except without the algebraically closed assumption. -/
+theorem isNilpotent_derivedSeries_of_traceForm_eq_zero_aux [IsAlgClosed K]
+    (h : traceForm K L M = 0) :
     IsNilpotent (derivedSeries K L 1) M := by
   /- By Engel's theorem it suffices to prove that `⁅L, L⁆` acts nilpotently on `M`. -/
   suffices ∀ x ∈ derivedSeries K L 1, _root_.IsNilpotent (φ x) from
@@ -82,7 +87,7 @@ public theorem isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (h : tra
     s.eigenspaces_iSupIndep hs_ss.iSup_eigenspace_eq_top
   let I := (ν : K) × Fin (finrank K (s.eigenspace ν))
   let v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K (s.eigenspace μ)
-  have : Fintype I := v.fintypeIndexOfRankLtAleph0 (rank_lt_aleph0 K M)
+  have : Fintype I := FiniteDimensional.fintypeBasisIndex v
   let μ : I → K := Sigma.fst
   have hsv (i : I) : s (v i) = μ i • v i :=
     mem_eigenspace_iff.mp (eigenDecomp.collectedBasis_mem _ i)
@@ -160,4 +165,23 @@ public theorem isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (h : tra
     exact Finset.sum_congr rfl <| by simp [toMatrix_apply, hyv, hsv]
   rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
 
+/-- If the trace form of `M` is zero, then the `⁅L, L⁆`-module `M` is nilpotent. -/
+public theorem isNilpotent_derivedSeries_of_traceForm_eq_zero (h : traceForm R L M = 0) :
+    IsNilpotent (derivedSeries R L 1) M := by
+  set A := AlgebraicClosure (FractionRing R)
+  have _i : FaithfulSMul R A := FaithfulSMul.trans R (FractionRing R) A
+  have nilp_ext : IsNilpotent (derivedSeries A (A ⊗[R] L) 1) (A ⊗[R] M) :=
+    isNilpotent_derivedSeries_of_traceForm_eq_zero_aux <| by simpa
+  rw [isNilpotent_iff_forall' (R := R)]
+  rw [isNilpotent_iff_forall' (R := A)] at nilp_ext
+  intro ⟨x, hx⟩
+  have hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1 := by
+    rw [derivedSeries_baseChange]
+    exact Submodule.tmul_mem_baseChange_of_mem 1 hx
+  have hbc_inj : Injective (End.baseChangeHom R A M) := LinearMap.baseChangeHom_injective R M A
+  have aux : (toEnd R (derivedSeries R L 1) M ⟨x, hx⟩).baseChangeHom R A M =
+      (toEnd R L M x).baseChange A := rfl
+  rw [← IsNilpotent.map_iff hbc_inj, aux, ← toEnd_baseChange]
+  exact nilp_ext ⟨_, hx_ext⟩
+
 end LieModule

Mathlib/Algebra/Lie/TraceForm.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Lie.InvariantForm
 public import Mathlib.Algebra.Lie.Weights.Cartan
 public import Mathlib.Algebra.Lie.Weights.Linear
 public import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
 public import Mathlib.LinearAlgebra.PID
 
 /-!
@@ -105,6 +106,12 @@ lemma traceForm_lieInvariant : (traceForm R L M).lieInvariant L := by
   apply LinearMap.isNilpotent_trace_of_isNilpotent
   exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y
 
+open scoped TensorProduct in
+@[simp] lemma traceForm_baseChange [Module.Free R M] [Module.Finite R M]
+    (A : Type*) [CommRing A] [Algebra R A] :
+    traceForm A (A ⊗[R] L) (A ⊗[R] M) = (traceForm R L M).baseChange A := by
+  ext; simp [traceForm_apply_apply, ← LinearMap.baseChange_comp, Algebra.algebraMap_eq_smul_one]
+
 variable {R L M} in
 lemma trace_toEnd_mul_eq_zero_of_traceForm_eq_zero (h : traceForm R L M = 0)
     (y : End R M) (hy : ∀ z ∈ LieHom.range φ, ⁅y, z⁆ ∈ LieHom.range φ)

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -142,6 +142,14 @@ theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂)
     B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') :=
   rfl
 
+@[simp] lemma baseChange_zero : (0 : BilinForm R M₂).baseChange A = 0 := by ext; simp
+
+@[simp] lemma baseChange_eq_zero_iff [FaithfulSMul R A]
+    (B : BilinForm R M₂) : B.baseChange A = 0 ↔ B = 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  ext m m'
+  simpa [← Algebra.algebraMap_eq_smul_one] using LinearMap.congr_fun₂ h (1 ⊗ₜ[R] m) (1 ⊗ₜ[R] m')
+
 variable (A) in
 /-- The base change of a symmetric bilinear form is symmetric. -/
 lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm :=

Mathlib/RingTheory/Flat/Basic.lean

@@ -71,7 +71,7 @@ open TensorProduct
 
 namespace Module
 
-open Function (Surjective)
+open Function (Injective Surjective)
 
 open LinearMap Submodule DirectSum
 
@@ -242,12 +242,35 @@ instance {S} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M]
 
 example [Flat R M] [Flat R N] : Flat R (M ⊗[R] N) := inferInstance
 
-theorem linearIndependent_one_tmul {S} [Semiring S] [Algebra R S] [Flat R S] {ι} {v : ι → M}
+section Algebra
+
+variable {S : Type*} [Semiring S] [Algebra R S]
+
+theorem linearIndependent_one_tmul [Flat R S] {ι} {v : ι → M}
     (hv : LinearIndependent R v) : LinearIndependent S ((1 : S) ⊗ₜ[R] v ·) := by
   classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
     Finsupp.linearCombination_one_tmul]
   simpa using lTensor_preserves_injective_linearMap _ hv
 
+variable (R S M)
+
+/-- See also `Module.FaithfullyFlat.tensorProduct_mk_injective`. -/
+lemma tensorProduct_mk_injective [FaithfulSMul R S] [Flat R M] :
+    Injective (TensorProduct.mk R S M 1) := by
+  have : TensorProduct.mk R S M 1 =
+      (Algebra.linearMap R S).rTensor M ∘ (TensorProduct.lid R M).symm := by ext; simp
+  rw [this]
+  refine Injective.comp ?_ (LinearEquiv.injective _)
+  exact Flat.rTensor_preserves_injective_linearMap _ <| FaithfulSMul.algebraMap_injective R S
+
+lemma _root_.LinearMap.baseChangeHom_injective [FaithfulSMul R S] [Flat R N] :
+    Injective (LinearMap.baseChangeHom R S M N) := by
+  intro f g h
+  ext m
+  simpa using Flat.tensorProduct_mk_injective R N S <| LinearMap.congr_fun h (1 ⊗ₜ[R] m)
+
+end Algebra
+
 end Flat
 
 end Semiring

Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean

@@ -76,7 +76,9 @@ lemma Module.FaithfullyFlat.of_flat_of_isLocalHom [IsLocalRing A] [IsLocalRing B
 variable [Module.FaithfullyFlat A B]
 
 /-- If `B` is a faithfully flat `A`-module and `M` is any `A`-module, the canonical
-map `M →ₗ[A] B ⊗[A] M` is injective. -/
+map `M →ₗ[A] B ⊗[A] M` is injective.
+
+See also `Module.Flat.tensorProduct_mk_injective`. -/
 lemma Module.FaithfullyFlat.tensorProduct_mk_injective (M : Type*) [AddCommGroup M] [Module A M] :
     Function.Injective (TensorProduct.mk A B M 1) := by
   rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]