feat(algebra/lie/nilpotent): generalise lower central series to start with given Lie submodule (#11625)

The advantage of this approach is that we can regard the terms of the lower central series of a Lie submodule as Lie submodules of the enclosing Lie module.

In particular, this is useful when considering the lower central series of a Lie ideal.

Author: ocfnash

src/algebra/lie/ideal_operations.lean

@@ -35,10 +35,11 @@ universes u v w w₁ w₂
 
 namespace lie_submodule
 
-variables {R : Type u} {L : Type v} {M : Type w}
-variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
-variables [lie_ring_module L M] [lie_module R L M]
-variables (N N' : lie_submodule R L M) (I J : lie_ideal R L)
+variables {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁}
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+variables [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂]
+variables (N N' : lie_submodule R L M) (I J : lie_ideal R L) (N₂ : lie_submodule R L M₂)
 
 section lie_ideal_operations
 
@@ -158,10 +159,9 @@ 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⁆ :=
+variables (f : M →ₗ⁅R,L⁆ M₂)
+
+lemma map_bracket_eq : 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],
@@ -176,6 +176,37 @@ begin
     exact ⟨⁅x, n⁆, ⟨x, ⟨n, hn⟩, rfl⟩, by simp⟩, },
 end
 
+lemma map_comap_le : map f (comap f N₂) ≤ N₂ :=
+(N₂ : set M₂).image_preimage_subset f
+
+lemma map_comap_eq (hf : N₂ ≤ f.range) : map f (comap f N₂) = N₂ :=
+begin
+  rw set_like.ext'_iff,
+  exact set.image_preimage_eq_of_subset hf,
+end
+
+lemma le_comap_map : N ≤ comap f (map f N) :=
+(N : set M).subset_preimage_image f
+
+lemma comap_map_eq (hf : f.ker = ⊥) : comap f (map f N) = N :=
+begin
+  rw set_like.ext'_iff,
+  exact (N : set M).preimage_image_eq (f.ker_eq_bot.mp hf),
+end
+
+lemma comap_bracket_eq (hf₁ : f.ker = ⊥) (hf₂ : N₂ ≤ f.range) :
+  comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆ :=
+begin
+  conv_lhs { rw ← map_comap_eq N₂ f hf₂, },
+  rw [← map_bracket_eq, comap_map_eq _ f hf₁],
+end
+
+@[simp] lemma map_comap_incl : map N.incl (comap N.incl N') = N ⊓ N' :=
+begin
+  rw ← coe_to_submodule_eq_iff,
+  exact (N : submodule R M).map_comap_subtype N',
+end
+
 end lie_ideal_operations
 
 end lie_submodule

src/algebra/lie/nilpotent.lean

@@ -26,20 +26,88 @@ lie algebra, lower central series, nilpotent
 
 universes u v w w₁ w₂
 
-namespace lie_module
+section nilpotent_modules
 
-variables (R : Type u) (L : Type v) (M : Type w)
+variables {R : Type u} {L : Type v} {M : Type w}
 variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
 variables [lie_ring_module L M] [lie_module R L M]
+variables (k : ℕ) (N : lie_submodule R L M)
+
+namespace lie_submodule
+
+/-- A generalisation of the lower central series. The zeroth term is a specified Lie submodule of
+a Lie module. In the case when we specify the top ideal `⊤` of the Lie algebra, regarded as a Lie
+module over itself, we get the usual lower central series of a Lie algebra.
+
+It can be more convenient to work with this generalisation when considering the lower central series
+of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic
+expression of the fact that the terms of the Lie submodule's lower central series are also Lie
+submodules of the enclosing Lie module.
+
+See also `lie_module.lower_central_series_eq_lcs_comap` and
+`lie_module.lower_central_series_map_eq_lcs` below. -/
+def lcs : lie_submodule R L M → lie_submodule R L M := (λ N, ⁅(⊤ : lie_ideal R L), N⁆)^[k]
+
+@[simp] lemma lcs_zero (N : lie_submodule R L M) : N.lcs 0 = N := rfl
+
+@[simp] lemma lcs_succ : N.lcs (k + 1) = ⁅(⊤ : lie_ideal R L), N.lcs k⁆ :=
+function.iterate_succ_apply' (λ N', ⁅⊤, N'⁆) k N
+
+end lie_submodule
+
+namespace lie_module
+
+variables (R L M)
 
 /-- The lower central series of Lie submodules of a Lie module. -/
-def lower_central_series (k : ℕ) : lie_submodule R L M := (λ I, ⁅(⊤ : lie_ideal R L), I⁆)^[k] ⊤
+def lower_central_series : lie_submodule R L M := (⊤ : lie_submodule R L M).lcs k
 
 @[simp] lemma lower_central_series_zero : lower_central_series R L M 0 = ⊤ := rfl
 
-@[simp] lemma lower_central_series_succ (k : ℕ) :
+@[simp] lemma lower_central_series_succ :
   lower_central_series R L M (k + 1) = ⁅(⊤ : lie_ideal R L), lower_central_series R L M k⁆ :=
-function.iterate_succ_apply' (λ I, ⁅(⊤ : lie_ideal R L), I⁆) k ⊤
+(⊤ : lie_submodule R L M).lcs_succ k
+
+end lie_module
+
+namespace lie_submodule
+
+open lie_module
+
+variables {R L M}
+
+lemma lcs_le_self : N.lcs k ≤ N :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp only [lcs_succ],
+    exact (lie_submodule.mono_lie_right _ _ ⊤ ih).trans (N.lie_le_right ⊤), },
+end
+
+lemma lower_central_series_eq_lcs_comap :
+  lower_central_series R L N k = (N.lcs k).comap N.incl :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp only [lcs_succ, lower_central_series_succ] at ⊢ ih,
+    have : N.lcs k ≤ N.incl.range,
+    { rw N.range_incl,
+      apply lcs_le_self, },
+    rw [ih, lie_submodule.comap_bracket_eq _ _ N.incl N.ker_incl this], },
+end
+
+lemma lower_central_series_map_eq_lcs :
+  (lower_central_series R L N k).map N.incl = N.lcs k :=
+begin
+  rw [lower_central_series_eq_lcs_comap, lie_submodule.map_comap_incl, inf_eq_right],
+  apply lcs_le_self,
+end
+
+end lie_submodule
+
+namespace lie_module
+
+variables (R L M)
 
 lemma antitone_lower_central_series : antitone $ lower_central_series R L M :=
 begin
@@ -227,6 +295,8 @@ set.nontrivial_mono
 
 end lie_module
 
+end nilpotent_modules
+
 @[priority 100]
 instance lie_algebra.is_solvable_of_is_nilpotent (R : Type u) (L : Type v)
   [comm_ring R] [lie_ring L] [lie_algebra R L] [hL : lie_module.is_nilpotent R L L] :

src/algebra/lie/submodule.lean

@@ -404,6 +404,8 @@ def incl : N →ₗ⁅R,L⁆ M :=
 { map_lie' := λ x m, rfl,
   ..submodule.subtype (N : submodule R M) }
 
+@[simp] lemma incl_coe : (N.incl : N →ₗ[R] M) = (N : submodule R M).subtype := rfl
+
 @[simp] lemma incl_apply (m : N) : N.incl m = m := rfl
 
 lemma incl_eq_val : (N.incl : N → M) = subtype.val := rfl
@@ -525,6 +527,10 @@ def comap : lie_submodule R L M :=
 { lie_mem := λ x m h, by { suffices : ⁅x, f m⁆ ∈ N', { simp [this], }, apply N'.lie_mem h, },
   ..(N' : submodule R M').comap (f : M →ₗ[R] M') }
 
+@[simp] lemma coe_submodule_comap :
+  (N'.comap f : submodule R M) = (N' : submodule R M').comap (f : M →ₗ[R] M') :=
+rfl
+
 variables {f N N₂ N'}
 
 lemma map_le_iff_le_comap : map f N ≤ N' ↔ N ≤ comap f N' :=
@@ -866,6 +872,12 @@ 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 ⊥
 
+@[simp] lemma ker_coe_submodule : (f.ker : submodule R M) = (f : M →ₗ[R] N).ker := rfl
+
+lemma ker_eq_bot : f.ker = ⊥ ↔ function.injective f :=
+by rw [← lie_submodule.coe_to_submodule_eq_iff, ker_coe_submodule, lie_submodule.bot_coe_submodule,
+  linear_map.ker_eq_bot, coe_to_linear_map]
+
 variables {f}
 
 @[simp] lemma mem_ker (m : M) : m ∈ f.ker ↔ f m = 0 := iff.rfl
@@ -898,6 +910,24 @@ by { ext, simp [lie_submodule.mem_map], }
 
 end lie_module_hom
 
+namespace lie_submodule
+
+variables {R : Type u} {L : Type v} {M : Type w}
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+variables (N : lie_submodule R L M)
+
+@[simp] lemma ker_incl : N.incl.ker = ⊥ :=
+by simp [← lie_submodule.coe_to_submodule_eq_iff]
+
+@[simp] lemma range_incl : N.incl.range = N :=
+by simp [← lie_submodule.coe_to_submodule_eq_iff]
+
+@[simp] lemma comap_incl_self : comap N.incl N = ⊤ :=
+by simp [← lie_submodule.coe_to_submodule_eq_iff]
+
+end lie_submodule
+
 section top_equiv_self
 
 variables {R : Type u} {L : Type v}