[Merged by Bors] - feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras

src/algebra/lie/cartan_subalgebra.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2021 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import algebra.lie.nilpotent
+
+/-!
+# Cartan subalgebras
+
+Cartan subalgebras are one of the most important concepts in Lie theory. We define them here.
+The standard example is the set of diagonal matrices in the Lie algebra of matrices.
+
+## Main definitions
+
+  * `lie_subalgebra.normalizer`
+  * `lie_subalgebra.le_normalizer_of_exists_ideal`
+  * `lie_subalgebra.is_cartan_subalgebra`
+
+## Tags
+
+lie subalgebra, normalizer, idealizer, cartan subalgebra
+-/
+
+universes u v w w₁ w₂
+
+variables {R : Type u} {L : Type v}
+variables [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L)
+
+namespace lie_subalgebra
+
+/-- The normalizer of a Lie subalgebra `H` is the set of elements of the Lie algebra whose product
+with any element of `H` lies in `H`. It is the Lie algebra equivalent of the group-theoretic
+normalizer (see `subgroup.normalizer`) and is an idealizer in the sense of abstract algebra. -/
+def normalizer : lie_subalgebra R L :=
+{ carrier   := { x : L | ∀ (y : L), (y ∈ H) → ⁅x, y⁆ ∈ H },
+  zero_mem' := λ y hy, by { rw zero_lie y, exact H.zero_mem, },
+  add_mem'  := λ z₁ z₂ h₁ h₂ y hy, by { rw add_lie, exact H.add_mem (h₁ y hy) (h₂ y hy), },
+  smul_mem' := λ t y hy z hz, by { rw smul_lie, exact H.smul_mem t (hy z hz), },
+  lie_mem'  := λ z₁ z₂ h₁ h₂ y hy, by
+    { rw lie_lie, exact H.sub_mem (h₁ _ (h₂ y hy)) (h₂ _ (h₁ y hy)), }, }
+
+lemma mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ (y : L), (y ∈ H) → ⁅x, y⁆ ∈ H := iff.rfl
+
+lemma le_normalizer : H ≤ H.normalizer :=
+begin
+  rw le_def, intros x hx,
+  simp only [submodule.mem_coe, mem_coe_submodule, coe_coe, mem_normalizer_iff] at ⊢ hx,
+  intros y, exact H.lie_mem hx,
+end
+
+/-- A Lie subalgebra is an ideal of its normalizer. -/
+lemma ideal_in_normalizer : ∃ (I : lie_ideal R H.normalizer), ↑I = of_le H.le_normalizer :=
+begin
+  simp only [exists_nested_lie_ideal_coe_eq_iff, mem_normalizer_iff],
+  intros x y h hy, exact h y hy,
+end
+
+/-- The normalizer of a Lie subalgebra `H` is the maximal Lie subalgebra in which `H` is a Lie
+ideal. -/
+lemma le_normalizer_of_exists_ideal {N : lie_subalgebra R L}
+  (h₁ : H ≤ N) (h₂ : ∃ (I : lie_ideal R N), ↑I = of_le h₁) : N ≤ H.normalizer :=
+begin
+  intros x hx,
+  rw mem_normalizer_iff,
+  intros y hy,
+  rw exists_nested_lie_ideal_coe_eq_iff at h₂,
+  exact h₂ x y hx hy,
+end
+
+variables (R L)
+
+/-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra. -/
+class is_cartan_subalgebra :=
+(nilpotent : lie_algebra.is_nilpotent R H)
+(self_normalizing : H.normalizer = H)
+
+end lie_subalgebra
+
+@[simp] lemma lie_ideal.normalizer_eq_top {R : Type u} {L : Type v}
+  [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
+  (I : lie_subalgebra R L).normalizer = ⊤ :=
+begin
+  ext x, simp only [lie_subalgebra.mem_normalizer_iff, lie_subalgebra.mem_top, iff_true],
+  intros y hy, exact I.lie_mem hy,
+end
+
+open lie_ideal
+
+/-- A nilpotent Lie algebra is its own Cartan subalgebra. -/
+instance lie_algebra.top_is_cartan_subalgebra_of_nilpotent [lie_algebra.is_nilpotent R L] :
+  lie_subalgebra.is_cartan_subalgebra R L ⊤ :=
+{ nilpotent        :=
+    by { rwa lie_algebra.nilpotent_iff_equiv_nilpotent lie_subalgebra.top_equiv_self, },
+  self_normalizing :=
+    by { rw [← top_coe_lie_subalgebra, normalizer_eq_top, top_coe_lie_subalgebra], }, }

src/algebra/lie/ideal_operations.lean

@@ -171,6 +171,21 @@ begin
   exact lie_submodule.lie_mem_lie _ _ fy₁ fy₂,
 end
 
+lemma map_bracket_eq {I₁ I₂ : lie_ideal R L} (h : function.surjective f) :
+  map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆ :=
+begin
+  suffices : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆, { exact le_antisymm (map_bracket_le f) this, },
+  rw [← lie_submodule.coe_submodule_le_coe_submodule, coe_map_of_surjective h,
+    lie_submodule.lie_ideal_oper_eq_linear_span,
+    lie_submodule.lie_ideal_oper_eq_linear_span, submodule.map_span],
+  apply submodule.span_mono,
+  rintros x ⟨⟨z₁, h₁⟩, ⟨z₂, h₂⟩, rfl⟩,
+  obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁,
+  obtain ⟨y₂, rfl⟩ := mem_map_of_surjective h h₂,
+  use [⁅(y₁ : L), (y₂ : L)⁆, y₁, y₂],
+  apply f.map_lie,
+end
+
 lemma comap_bracket_le {J₁ J₂ : lie_ideal R L'} : ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆ :=
 begin
   rw ← map_le_iff_le_comap,

src/algebra/lie/nilpotent.lean

@@ -78,3 +78,70 @@ begin
   use k, rw ← le_bot_iff at h ⊢,
   exact le_trans (lie_module.derived_series_le_lower_central_series R L k) h,
 end
+
+section nilpotent_algebras
+
+-- TODO Generalise the below to Lie modules if / when we define morphisms, equivs of Lie modules
+-- covering a Lie algebra morphism of (possibly different) Lie algebras.
+
+variables (R : Type u) (L : Type v) (L' : Type w)
+variables [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L']
+
+/-- We say a Lie algebra is nilpotent when it is nilpotent as a Lie module over itself via the
+adjoint representation. -/
+abbreviation lie_algebra.is_nilpotent (R : Type u) (L : Type v)
+  [comm_ring R] [lie_ring L] [lie_algebra R L] : Prop :=
+lie_module.is_nilpotent R L L
+
+variables {R L L'}
+open lie_algebra
+open lie_module (lower_central_series)
+
+lemma lie_ideal.lower_central_series_map_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,
+  { simp only [lie_module.lower_central_series_zero, le_top], },
+  { simp only [lie_module.lower_central_series_succ],
+    exact le_trans (lie_ideal.map_bracket_le f) (lie_submodule.mono_lie _ _ _ _ le_top ih), },
+end
+
+lemma lie_ideal.lower_central_series_map_eq (k : ℕ) {f : L →ₗ⁅R⁆ L'}
+  (h : function.surjective f) :
+  lie_ideal.map f (lower_central_series R L L k) = lower_central_series R L' L' k :=
+begin
+  have h' : (⊤ : lie_ideal R L).map f = ⊤, { exact f.ideal_range_eq_top_of_surjective h, },
+  induction k with k ih,
+  { simp only [lie_module.lower_central_series_zero], exact h', },
+  { simp only [lie_module.lower_central_series_succ, lie_ideal.map_bracket_eq f h, ih, h'], },
+end
+
+lemma function.injective.lie_algebra_is_nilpotent [h₁ : is_nilpotent R L'] {f : L →ₗ⁅R⁆ L'}
+  (h₂ : function.injective f) : is_nilpotent R L :=
+{ nilpotent :=
+    begin
+      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,
+    end, }
+
+lemma function.surjective.lie_algebra_is_nilpotent [h₁ : is_nilpotent R L] {f : L →ₗ⁅R⁆ L'}
+  (h₂ : function.surjective f) : is_nilpotent R L' :=
+{ nilpotent :=
+    begin
+      tactic.unfreeze_local_instances, obtain ⟨k, hk⟩ := h₁,
+      use k,
+      rw [← lie_ideal.lower_central_series_map_eq k h₂, hk],
+      simp only [lie_hom.map_bot_iff, bot_le],
+    end, }
+
+lemma lie_algebra.nilpotent_iff_equiv_nilpotent (e : L ≃ₗ⁅R⁆ L') :
+  is_nilpotent R L ↔ is_nilpotent R L' :=
+begin
+  split; introsI h,
+  { exact e.symm.injective.lie_algebra_is_nilpotent, },
+  { exact e.injective.lie_algebra_is_nilpotent, },
+end
+
+end nilpotent_algebras

src/algebra/lie/semisimple.lean

@@ -80,7 +80,7 @@ begin
   intros I hI,
   tactic.unfreeze_local_instances, obtain ⟨h₁, h₂⟩ := h,
   by_contradiction contra,
-  rw [h₁ I contra, lie_abelian_iff_equiv_lie_abelian top_equiv_self] at hI,
+  rw [h₁ I contra, lie_abelian_iff_equiv_lie_abelian lie_ideal.top_equiv_self] at hI,
   exact h₂ hI,
 end
 

src/algebra/lie/solvable.lean

@@ -214,7 +214,7 @@ variables (R L)
 instance of_abelian_is_solvable [is_lie_abelian L] : is_solvable R L :=
 begin
   use 1,
-  rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian top_equiv_self],
+  rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian lie_ideal.top_equiv_self],
   apply_instance,
 end
 

src/algebra/lie/subalgebra.lean

@@ -75,6 +75,9 @@ lemma smul_mem (t : R) {x : L} (h : x ∈ L') : t • x ∈ L' := (L' : submodul
 lemma add_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (x + y : L) ∈ L' :=
 (L' : submodule R L).add_mem hx hy
 
+lemma sub_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (x - y : L) ∈ L' :=
+(L' : submodule R L).sub_mem hx hy
+
 lemma lie_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (⁅x, y⁆ : L) ∈ L' := L'.lie_mem' hx hy
 
 @[simp] lemma mem_carrier {x : L} : x ∈ L'.carrier ↔ x ∈ (L' : set L) := iff.rfl

src/algebra/lie/submodule.lean

@@ -422,6 +422,8 @@ namespace lie_ideal
 
 variables (f : L →ₗ⁅R⁆ L') (I : lie_ideal R L) (J : lie_ideal R L')
 
+@[simp] lemma top_coe_lie_subalgebra : ((⊤ : lie_ideal R L) : lie_subalgebra R L) = ⊤ := rfl
+
 /-- A morphism of Lie algebras `f : L → L'` pushes forward Lie ideals of `L` to Lie ideals of `L'`.
 
 Note that unlike `lie_submodule.map`, we must take the `lie_span` of the image. Mathematically
@@ -563,12 +565,64 @@ 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]
 
+@[simp] lemma range_coe_submodule : (f.range : submodule R L') = (f : L →ₗ[R] L').range := rfl
+
+lemma range_eq_top : f.range = ⊤ ↔ function.surjective f :=
+begin
+  rw [← lie_subalgebra.coe_to_submodule_eq_iff, range_coe_submodule,
+    lie_subalgebra.top_coe_submodule],
+  exact linear_map.range_eq_top,
+end
+
+@[simp] lemma ideal_range_eq_top_of_surjective (h : function.surjective f) : f.ideal_range = ⊤ :=
+begin
+  rw ← f.range_eq_top at h,
+  rw [ideal_range_eq_lie_span_range, h, ← lie_subalgebra.coe_to_submodule,
+    ← lie_submodule.coe_to_submodule_eq_iff, lie_submodule.top_coe_submodule,
+      lie_subalgebra.top_coe_submodule, lie_submodule.coe_lie_span_submodule_eq_iff],
+  use ⊤,
+  exact lie_submodule.top_coe_submodule,
+end
+
+lemma is_ideal_morphism_of_surjective (h : function.surjective f) : f.is_ideal_morphism :=
+by rw [is_ideal_morphism_def, f.ideal_range_eq_top_of_surjective h, f.range_eq_top.mpr h,
+    lie_ideal.top_coe_lie_subalgebra]
+
 end lie_hom
 
 namespace lie_ideal
 
 variables {f : L →ₗ⁅R⁆ L'} {I : lie_ideal R L} {J : lie_ideal R L'}
 
+lemma coe_map_of_surjective (h : function.surjective f) :
+  (I.map f : submodule R L') = (I : submodule R L).map f :=
+begin
+  let J : lie_ideal R L' :=
+  { lie_mem := λ x y hy,
+    begin
+      have hy' : ∃ (x : L), x ∈ I ∧ f x = y, { simpa [hy], },
+      obtain ⟨z₂, hz₂, rfl⟩ := hy',
+      obtain ⟨z₁, rfl⟩ := h x,
+      simp only [lie_hom.coe_to_linear_map, submodule.mem_coe, set.mem_image,
+        lie_submodule.mem_coe_submodule, submodule.mem_carrier, submodule.map_coe],
+      use ⁅z₁, z₂⁆,
+      exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩,
+    end,
+    ..(I : submodule R L).map (f : L →ₗ[R] L'), },
+  erw lie_submodule.coe_lie_span_submodule_eq_iff,
+  use J,
+  apply lie_submodule.coe_to_submodule_mk,
+end
+
+lemma mem_map_of_surjective {y : L'} (h₁ : function.surjective f) (h₂ : y ∈ I.map f) :
+  ∃ (x : I), f x = y :=
+begin
+  rw [← lie_submodule.mem_coe_submodule, coe_map_of_surjective h₁, submodule.mem_map] at h₂,
+  obtain ⟨x, hx, rfl⟩ := h₂,
+  use ⟨x, hx⟩,
+  refl,
+end
+
 lemma bot_of_map_eq_bot {I : lie_ideal R L} (h₁ : function.injective f) (h₂ : I.map f = ⊥) :
   I = ⊥ :=
 begin
@@ -593,7 +647,7 @@ lemma hom_of_le_injective {I₁ I₂ : lie_ideal R L} (h : I₁ ≤ I₂) :
 λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, submodule.coe_eq_coe,
   subtype.val_eq_coe]
 
-lemma map_sup_ker_eq_map : lie_ideal.map f (I ⊔ f.ker) = lie_ideal.map f I :=
+@[simp] lemma map_sup_ker_eq_map : lie_ideal.map f (I ⊔ f.ker) = lie_ideal.map f I :=
 begin
   suffices : lie_ideal.map f (I ⊔ f.ker) ≤ lie_ideal.map f I,
   { exact le_antisymm this (lie_ideal.map_mono le_sup_left), },
@@ -653,18 +707,26 @@ end lie_ideal
 
 end lie_submodule_map_and_comap
 
-namespace lie_algebra
+section top_equiv_self
 
 variables {R : Type u} {L : Type v}
 variables [comm_ring R] [lie_ring L] [lie_algebra R L]
 
-/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie algebra. -/
-def top_equiv_self : (⊤ : lie_ideal R L) ≃ₗ⁅R⁆ L :=
+/-- The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra. -/
+def lie_subalgebra.top_equiv_self : (⊤ : lie_subalgebra R L) ≃ₗ⁅R⁆ L :=
 { inv_fun   := λ x, ⟨x, set.mem_univ x⟩,
   left_inv  := λ x, by { ext, refl, },
   right_inv := λ x, rfl,
-  ..(⊤ : lie_ideal R L).incl, }
+  ..(⊤ : lie_subalgebra R L).incl, }
+
+@[simp] lemma lie_subalgebra.top_equiv_self_apply (x : (⊤ : lie_subalgebra R L)) :
+  lie_subalgebra.top_equiv_self x = x := rfl
+
+/-- The natural equivalence between the 'top' Lie ideal and the enclosing Lie algebra. -/
+def lie_ideal.top_equiv_self : (⊤ : lie_ideal R L) ≃ₗ⁅R⁆ L :=
+lie_subalgebra.top_equiv_self
 
-@[simp] lemma top_equiv_self_apply (x : (⊤ : lie_ideal R L)) : top_equiv_self x = x := rfl
+@[simp] lemma lie_ideal.top_equiv_self_apply (x : (⊤ : lie_ideal R L)) :
+  lie_ideal.top_equiv_self x = x := rfl
 
-end lie_algebra
+end top_equiv_self