feat(algebra/lie/nilpotent): central extensions of nilpotent Lie modu…

…les / algebras are nilpotent (#11422)

The main result is `lie_algebra.nilpotent_of_nilpotent_quotient`.

src/algebra/lie/abelian.lean

@@ -114,6 +114,15 @@ iff.rfl
 instance : is_trivial L (max_triv_submodule R L M) :=
 { trivial := λ x m, subtype.ext (m.property x), }
 
+@[simp] lemma ideal_oper_max_triv_submodule_eq_bot (I : lie_ideal R L) :
+  ⁅I, max_triv_submodule R L M⁆ = ⊥ :=
+begin
+  rw [← lie_submodule.coe_to_submodule_eq_iff, lie_submodule.lie_ideal_oper_eq_linear_span,
+    lie_submodule.bot_coe_submodule, submodule.span_eq_bot],
+  rintros m ⟨⟨x, hx⟩, ⟨⟨m, hm⟩, rfl⟩⟩,
+  exact hm x,
+end
+
 lemma trivial_iff_le_maximal_trivial (N : lie_submodule R L M) :
   is_trivial L N ↔ N ≤ max_triv_submodule R L M :=
 ⟨ λ h m hm x, is_trivial.dcases_on h (λ h, subtype.ext_iff.mp (h x ⟨m, hm⟩)),

src/algebra/lie/basic.lean

@@ -464,6 +464,15 @@ by simp only [sub_add_cancel, map_lie, lie_hom.lie_apply]
 @[simp] lemma map_zero (f : M →ₗ⁅R,L⁆ N) : f 0 = 0 :=
 linear_map.map_zero (f : M →ₗ[R] N)
 
+/-- The identity map is a morphism of Lie modules. -/
+def id : M →ₗ⁅R,L⁆ M :=
+{ map_lie' := λ x m, rfl,
+  .. (linear_map.id : M →ₗ[R] M) }
+
+@[simp] lemma coe_id : ((id : M →ₗ⁅R,L⁆ M) : M → M) = _root_.id := rfl
+
+lemma id_apply (x : M) : (id : M →ₗ⁅R,L⁆ M) x = x := rfl
+
 /-- The constant 0 map is a Lie module morphism. -/
 instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M →ₗ[R] N) }⟩
 
@@ -472,7 +481,7 @@ instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M
 lemma zero_apply (m : M) : (0 : M →ₗ⁅R,L⁆ N) m = 0 := rfl
 
 /-- The identity map is a Lie module morphism. -/
-instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie' := by simp, ..(1 : M →ₗ[R] M) }⟩
+instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨id⟩
 
 instance : inhabited (M →ₗ⁅R,L⁆ N) := ⟨0⟩
 

src/algebra/lie/ideal_operations.lean

@@ -150,6 +150,24 @@ by { rw le_inf_iff, split; apply mono_lie_right; [exact inf_le_left, exact inf_l
 @[simp] lemma inf_lie : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆ :=
 by { rw le_inf_iff, split; apply mono_lie_left; [exact inf_le_left, exact inf_le_right], }
 
+lemma map_bracket_eq
+  {M₂ : Type w₁} [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂]
+  (f : M →ₗ⁅R,L⁆ M₂) :
+  map f ⁅I, N⁆ = ⁅I, map f N⁆ :=
+begin
+  rw [← coe_to_submodule_eq_iff, coe_submodule_map, lie_ideal_oper_eq_linear_span,
+    lie_ideal_oper_eq_linear_span, submodule.map_span],
+  congr,
+  ext m,
+  split,
+  { rintros ⟨-, ⟨⟨x, ⟨n, hn⟩, rfl⟩, hm⟩⟩,
+    simp only [lie_module_hom.coe_to_linear_map, lie_module_hom.map_lie] at hm,
+    exact ⟨x, ⟨f n, (mem_map (f n)).mpr ⟨n, hn, rfl⟩⟩, hm⟩, },
+  { rintros ⟨x, ⟨m₂, hm₂ : m₂ ∈ map f N⟩, rfl⟩,
+    obtain ⟨n, hn, rfl⟩ := (mem_map m₂).mp hm₂,
+    exact ⟨⁅x, n⁆, ⟨x, ⟨n, hn⟩, rfl⟩, by simp⟩, },
+end
+
 end lie_ideal_operations
 
 end lie_submodule

src/algebra/lie/nilpotent.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import algebra.lie.solvable
+import algebra.lie.quotient
 import linear_algebra.eigenspace
 import ring_theory.nilpotent
 
@@ -58,6 +59,20 @@ begin
     exact lie_submodule.lie_mem_lie _ _ (lie_submodule.mem_top x) ih, },
 end
 
+variables {R L M}
+
+lemma map_lower_central_series_le
+  {M₂ : Type w₁} [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂]
+  (k : ℕ) (f : M →ₗ⁅R,L⁆ M₂) :
+  lie_submodule.map f (lower_central_series R L M k) ≤ lower_central_series R L M₂ k :=
+begin
+  induction k with k ih,
+  { simp only [lie_module.lower_central_series_zero, le_top], },
+  { simp only [lie_module.lower_central_series_succ, lie_submodule.map_bracket_eq],
+    exact lie_submodule.mono_lie_right _ _ ⊤ ih, },
+end
+
+variables (R L M)
 open lie_algebra
 
 lemma derived_series_le_lower_central_series (k : ℕ) :
@@ -106,6 +121,25 @@ begin
   exact linear_map.zero_apply m,
 end
 
+/-- If the quotient of a Lie module `M` by a Lie submodule on which the Lie algebra acts trivially
+is nilpotent then `M` is nilpotent.
+
+This is essentially the Lie module equivalent of the fact that a central
+extension of nilpotent Lie algebras is nilpotent. See `lie_algebra.nilpotent_of_nilpotent_quotient`
+below for the corresponding result for Lie algebras. -/
+lemma nilpotent_of_nilpotent_quotient {N : lie_submodule R L M}
+  (h₁ : N ≤ max_triv_submodule R L M) (h₂ : is_nilpotent R L (M ⧸ N)) : is_nilpotent R L M :=
+begin
+  unfreezingI { obtain ⟨k, hk⟩ := h₂, },
+  use k+1,
+  simp only [lower_central_series_succ],
+  suffices : lower_central_series R L M k ≤ N,
+  { replace this := lie_submodule.mono_lie_right _ _ ⊤ (le_trans this h₁),
+    rwa [ideal_oper_max_triv_submodule_eq_bot, le_bot_iff] at this, },
+  rw [← lie_submodule.quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← hk],
+  exact map_lower_central_series_le k (lie_submodule.quotient.mk' N),
+end
+
 end lie_module
 
 @[priority 100]
@@ -147,7 +181,41 @@ variables {R L L'}
 
 open lie_module (lower_central_series)
 
-lemma lie_ideal.lower_central_series_map_le (k : ℕ) {f : L →ₗ⁅R⁆ L'} :
+/-- Given an ideal `I` of a Lie algebra `L`, the lower central series of `L ⧸ I` is the same
+whether we regard `L ⧸ I` as an `L` module or an `L ⧸ I` module.
+
+TODO: This result obviously generalises but the generalisation requires the missing definition of
+morphisms between Lie modules over different Lie algebras. -/
+lemma coe_lower_central_series_ideal_quot_eq {I : lie_ideal R L} (k : ℕ) :
+  (lower_central_series R L (L ⧸ I) k : submodule R (L ⧸ I)) =
+  lower_central_series R (L ⧸ I) (L ⧸ I) k :=
+begin
+  induction k with k ih,
+  { simp only [lie_submodule.top_coe_submodule, lie_module.lower_central_series_zero], },
+  { simp only [lie_module.lower_central_series_succ, lie_submodule.lie_ideal_oper_eq_linear_span],
+    congr,
+    ext x,
+    split,
+    { rintros ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩,
+      erw [← lie_submodule.mem_coe_submodule, ih, lie_submodule.mem_coe_submodule] at hz,
+      exact ⟨⟨lie_submodule.quotient.mk y, submodule.mem_top⟩, ⟨z, hz⟩, rfl⟩, },
+    { rintros ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩,
+      erw [← lie_submodule.mem_coe_submodule, ← ih, lie_submodule.mem_coe_submodule] at hz,
+      exact ⟨⟨y, submodule.mem_top⟩, ⟨z, hz⟩, rfl⟩, }, },
+end
+
+/-- A central extension of nilpotent Lie algebras is nilpotent. -/
+lemma lie_algebra.nilpotent_of_nilpotent_quotient {I : lie_ideal R L}
+  (h₁ : I ≤ center R L) (h₂ : is_nilpotent R (L ⧸ I)) : is_nilpotent R L :=
+begin
+  suffices : lie_module.is_nilpotent R L (L ⧸ I),
+  { exact lie_module.nilpotent_of_nilpotent_quotient R L L h₁ this, },
+  unfreezingI { obtain ⟨k, hk⟩ := h₂, },
+  use k,
+  simp [← lie_submodule.coe_to_submodule_eq_iff, coe_lower_central_series_ideal_quot_eq, hk],
+end
+
+lemma lie_ideal.map_lower_central_series_le (k : ℕ) {f : L →ₗ⁅R⁆ L'} :
   lie_ideal.map f (lower_central_series R L L k) ≤ lower_central_series R L' L' k :=
 begin
   induction k with k ih,
@@ -175,7 +243,7 @@ lemma function.injective.lie_algebra_is_nilpotent [h₁ : is_nilpotent R L'] {f
     tactic.unfreeze_local_instances, obtain ⟨k, hk⟩ := h₁,
     use k,
     apply lie_ideal.bot_of_map_eq_bot h₂, rw [eq_bot_iff, ← hk],
-    apply lie_ideal.lower_central_series_map_le,
+    apply lie_ideal.map_lower_central_series_le,
   end, }
 
 lemma function.surjective.lie_algebra_is_nilpotent [h₁ : is_nilpotent R L] {f : L →ₗ⁅R⁆ L'}

src/algebra/lie/quotient.lean

@@ -144,6 +144,15 @@ instance lie_quotient_lie_algebra : lie_algebra R (L ⧸ I) :=
 def mk' : M →ₗ⁅R,L⁆ M ⧸ N :=
 { to_fun := mk, map_lie' := λ r m, rfl, ..N.to_submodule.mkq}
 
+@[simp] lemma mk_eq_zero {m : M} : mk' N m = 0 ↔ m ∈ N :=
+submodule.quotient.mk_eq_zero N.to_submodule
+
+@[simp] lemma mk'_ker : (mk' N).ker = N :=
+by { ext, simp, }
+
+@[simp] lemma map_mk'_eq_bot_le : map (mk' N) N' = ⊥ ↔ N' ≤ N :=
+by rw [← lie_module_hom.le_ker_iff_map, mk'_ker]
+
 /-- Two `lie_module_hom`s from a quotient lie module are equal if their compositions with
 `lie_submodule.quotient.mk'` are equal.
 

src/algebra/lie/submodule.lean

@@ -183,31 +183,33 @@ end
 
 namespace lie_subalgebra
 
-variables {L}
+variables {L} (K : lie_subalgebra R L)
 
 /-- Given a Lie subalgebra `K ⊆ L`, if we view `L` as a `K`-module by restriction, it contains
 a distinguished Lie submodule for the action of `K`, namely `K` itself. -/
-def to_lie_submodule (K : lie_subalgebra R L) : lie_submodule R K L :=
+def to_lie_submodule : lie_submodule R K L :=
 { lie_mem := λ x y hy, K.lie_mem x.property hy,
   .. (K : submodule R L) }
 
-@[simp] lemma coe_to_lie_submodule (K : lie_subalgebra R L) :
+@[simp] lemma coe_to_lie_submodule :
   (K.to_lie_submodule : submodule R L) = K :=
 by { rcases K with ⟨⟨⟩⟩, refl, }
 
-@[simp] lemma mem_to_lie_submodule {K : lie_subalgebra R L} (x : L) :
+variables {K}
+
+@[simp] lemma mem_to_lie_submodule (x : L) :
   x ∈ K.to_lie_submodule ↔ x ∈ K :=
 iff.rfl
 
-lemma exists_lie_ideal_coe_eq_iff (K : lie_subalgebra R L) :
+lemma exists_lie_ideal_coe_eq_iff :
   (∃ (I : lie_ideal R L), ↑I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K :=
 begin
   simp only [← coe_to_submodule_eq_iff, lie_ideal.coe_to_lie_subalgebra_to_submodule,
     submodule.exists_lie_submodule_coe_eq_iff L],
   exact iff.rfl,
 end
 
-lemma exists_nested_lie_ideal_coe_eq_iff {K K' : lie_subalgebra R L} (h : K ≤ K') :
+lemma exists_nested_lie_ideal_coe_eq_iff {K' : lie_subalgebra R L} (h : K ≤ K') :
   (∃ (I : lie_ideal R K'), ↑I = of_le h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K :=
 begin
   simp only [exists_lie_ideal_coe_eq_iff, coe_bracket, mem_of_le],
@@ -494,6 +496,10 @@ def map : lie_submodule R L M' :=
     { norm_cast at hfm, simp [hfm], }, },
   ..(N : submodule R M).map (f : M →ₗ[R] M') }
 
+@[simp] lemma coe_submodule_map :
+  (N.map f : submodule R M') = (N : submodule R M).map (f : M →ₗ[R] M') :=
+rfl
+
 /-- A morphism of Lie modules `f : M → M'` pulls back Lie submodules of `M'` to Lie submodules of
 `M`. -/
 def comap : lie_submodule R L M :=
@@ -838,6 +844,24 @@ variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L
 variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
 variables (f : M →ₗ⁅R,L⁆ N)
 
+/-- The kernel of a morphism of Lie algebras, as an ideal in the domain. -/
+def ker : lie_submodule R L M := lie_submodule.comap f ⊥
+
+variables {f}
+
+@[simp] lemma mem_ker (m : M) : m ∈ f.ker ↔ f m = 0 := iff.rfl
+
+@[simp] lemma ker_id : (lie_module_hom.id : M →ₗ⁅R,L⁆ M).ker = ⊥ := rfl
+
+@[simp] lemma comp_ker_incl : f.comp f.ker.incl = 0 :=
+by { ext ⟨m, hm⟩, exact (mem_ker m).mp hm, }
+
+lemma le_ker_iff_map (M' : lie_submodule R L M) :
+  M' ≤ f.ker ↔ lie_submodule.map f M' = ⊥ :=
+by rw [ker, eq_bot_iff, lie_submodule.map_le_iff_le_comap]
+
+variables (f)
+
 /-- The range of a morphism of Lie modules `f : M → N` is a Lie submodule of `N`.
 See Note [range copy pattern]. -/
 def range : lie_submodule R L N :=