[Merged by Bors] - feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule

src/algebra/lie/abelian.lean

@@ -123,6 +123,17 @@ begin
   exact hm x,
 end
 
+lemma le_max_triv_iff_bracket_eq_bot {N : lie_submodule R L M} :
+  N ≤ max_triv_submodule R L M ↔ ⁅(⊤ : lie_ideal R L), N⁆ = ⊥ :=
+begin
+  refine ⟨λ h, _, λ h m hm, _⟩,
+  { rw [← le_bot_iff, ← ideal_oper_max_triv_submodule_eq_bot R L M ⊤],
+    exact lie_submodule.mono_lie_right _ _ ⊤ h, },
+  { rw mem_max_triv_submodule,
+    rw lie_submodule.lie_eq_bot_iff at h,
+    exact λ x, h x (lie_submodule.mem_top x) m hm, },
+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/ideal_operations.lean

@@ -108,6 +108,14 @@ begin
   change x ∈ (⊥ : lie_ideal R L) at hx, rw mem_bot at hx, simp [hx],
 end
 
+lemma lie_eq_bot_iff : ⁅I, N⁆ = ⊥ ↔ ∀ (x ∈ I) (m ∈ N), ⁅(x : L), m⁆ = 0 :=
+begin
+  rw [lie_ideal_oper_eq_span, lie_submodule.lie_span_eq_bot_iff],
+  refine ⟨λ h x hx m hm, h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, _⟩,
+  rintros h - ⟨⟨x, hx⟩, ⟨⟨n, hn⟩, rfl⟩⟩,
+  exact h x hx n hn,
+end
+
 lemma mono_lie (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆ :=
 begin
   intros m h,

src/algebra/lie/nilpotent.lean

@@ -41,6 +41,18 @@ def lower_central_series (k : ℕ) : lie_submodule R L M := (λ I, ⁅(⊤ : lie
   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 ⊤
 
+lemma antitone_lower_central_series : antitone $ lower_central_series R L M :=
+begin
+  intros l k,
+  induction k with k ih generalizing l;
+  intros h,
+  { exact (le_zero_iff.mp h).symm ▸ le_refl _, },
+  { rcases nat.of_le_succ h with hk | hk,
+    { rw lower_central_series_succ,
+      exact (lie_submodule.mono_lie_right _ _ ⊤ (ih hk)).trans (lie_submodule.lie_le_right _ _), },
+    { exact hk.symm ▸ le_refl _, }, },
+end
+
 lemma trivial_iff_lower_central_eq_bot : is_trivial L M ↔ lower_central_series R L M 1 = ⊥ :=
 begin
   split; intros h,
@@ -140,6 +152,79 @@ begin
   exact map_lower_central_series_le k (lie_submodule.quotient.mk' N),
 end
 
+/-- Given a nilpotent Lie module `M` with lower central series `M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is
+the natural number `k` (the number of inclusions).
+
+For a non-nilpotent module, we use the junk value 0. -/
+noncomputable def nilpotency_length : ℕ :=
+Inf { k | lower_central_series R L M k = ⊥ }
+
+lemma nilpotency_length_eq_zero_iff [is_nilpotent R L M] :
+  nilpotency_length R L M = 0 ↔ subsingleton M :=
+begin
+  let s := { k | lower_central_series R L M k = ⊥ },
+  have hs : s.nonempty,
+  { unfreezingI { obtain ⟨k, hk⟩ := (by apply_instance : is_nilpotent R L M), },
+    exact ⟨k, hk⟩, },
+  change Inf s = 0 ↔ _,
+  rw [← lie_submodule.subsingleton_iff R L M, ← subsingleton_iff_bot_eq_top,
+      ← lower_central_series_zero, @eq_comm (lie_submodule R L M)],
+  refine ⟨λ h, h ▸ nat.Inf_mem hs, λ h, _⟩,
+  rw nat.Inf_eq_zero,
+  exact or.inl h,
+end
+
+lemma nilpotency_length_eq_succ_iff (k : ℕ) :
+  nilpotency_length R L M = k + 1 ↔
+  lower_central_series R L M (k + 1) = ⊥ ∧ lower_central_series R L M k ≠ ⊥ :=
+begin
+  let s := { k | lower_central_series R L M k = ⊥ },
+  change Inf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s,
+  have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s,
+  { rintros k₁ k₂ h₁₂ (h₁ : lower_central_series R L M k₁ = ⊥),
+    exact eq_bot_iff.mpr (h₁ ▸ antitone_lower_central_series R L M h₁₂), },
+  exact nat.Inf_upward_closed_eq_succ_iff hs k,
+end
+
+/-- Given a non-trivial nilpotent Lie module `M` with lower central series
+`M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is the `k-1`th term in the lower central series (the last
+non-trivial term).
+
+For a trivial or non-nilpotent module, this is the bottom submodule, `⊥`. -/
+noncomputable def lower_central_series_last : lie_submodule R L M :=
+match nilpotency_length R L M with
+| 0     := ⊥
+| k + 1 := lower_central_series R L M k
+end
+
+lemma lower_central_series_last_le_max_triv :
+  lower_central_series_last R L M ≤ max_triv_submodule R L M :=
+begin
+  rw lower_central_series_last,
+  cases h : nilpotency_length R L M with k,
+  { exact bot_le, },
+  { rw le_max_triv_iff_bracket_eq_bot,
+    rw [nilpotency_length_eq_succ_iff, lower_central_series_succ] at h,
+    exact h.1, },
+end
+
+lemma nontrivial_lower_central_series_last [nontrivial M] [is_nilpotent R L M] :
+  nontrivial (lower_central_series_last R L M) :=
+begin
+  rw [lie_submodule.nontrivial_iff_ne_bot, lower_central_series_last],
+  cases h : nilpotency_length R L M,
+  { rw [nilpotency_length_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h,
+    contradiction, },
+  { rw nilpotency_length_eq_succ_iff at h,
+    exact h.2, },
+end
+
+lemma nontrivial_max_triv_of_is_nilpotent [nontrivial M] [is_nilpotent R L M] :
+  nontrivial (max_triv_submodule R L M) :=
+set.nontrivial_mono
+  (lower_central_series_last_le_max_triv R L M)
+  (nontrivial_lower_central_series_last R L M)
+
 end lie_module
 
 @[priority 100]

src/algebra/lie/submodule.lean

@@ -379,6 +379,18 @@ not_iff_not.mp (
 
 instance [nontrivial M] : nontrivial (lie_submodule R L M) := (nontrivial_iff R L M).mpr ‹_›
 
+lemma nontrivial_iff_ne_bot {N : lie_submodule R L M} : nontrivial N ↔ N ≠ ⊥ :=
+begin
+  split;
+  contrapose!,
+  { rintros rfl ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : lie_submodule R L M)⟩,
+                 ⟨m₂, h₂ : m₂ ∈ (⊥ : lie_submodule R L M)⟩, h₁₂⟩,
+    simpa [(lie_submodule.mem_bot _).mp h₁, (lie_submodule.mem_bot _).mp h₂] using h₁₂, },
+  { rw [not_nontrivial_iff_subsingleton, lie_submodule.eq_bot_iff],
+    rintros ⟨h⟩ m hm,
+    simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩, },
+end
+
 variables {R L M}
 
 section inclusion_maps
@@ -462,6 +474,9 @@ protected def gi : galois_insertion (lie_span R L : set M → lie_submodule R L
 @[simp] lemma span_univ : lie_span R L (set.univ : set M) = ⊤ :=
 eq_top_iff.2 $ set_like.le_def.2 $ subset_lie_span
 
+lemma lie_span_eq_bot_iff : lie_span R L s = ⊥ ↔ ∀ (m ∈ s), m = (0 : M) :=
+by rw [_root_.eq_bot_iff, lie_span_le, bot_coe, subset_singleton_iff]
+
 variables {M}
 
 lemma span_union (s t : set M) : lie_span R L (s ∪ t) = lie_span R L s ⊔ lie_span R L t :=

src/data/set/basic.lean

@@ -247,6 +247,14 @@ mt $ mem_of_subset_of_mem h
 
 theorem not_subset : (¬ s ⊆ t) ↔ ∃a ∈ s, a ∉ t := by simp only [subset_def, not_forall]
 
+theorem nontrivial_mono {α : Type*} {s t : set α} (h₁ : s ⊆ t) (h₂ : nontrivial s) :
+  nontrivial t :=
+begin
+  rw nontrivial_iff at h₂ ⊢,
+  obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h₂,
+  exact ⟨⟨x, h₁ hx⟩, ⟨y, h₁ hy⟩, by simpa using hxy⟩,
+end
+
 /-! ### Definition of strict subsets `s ⊂ t` and basic properties. -/
 
 instance : has_ssubset (set α) := ⟨(<)⟩