feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras (#6385)

We do this via the normalizer of a Lie subalgebra, which is also defined here.

src/algebra/lie/cartan_subalgebra.lean

@@ -0,0 +1,92 @@
+/-
+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_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 bracket
+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 : ∀ (x y : L), x ∈ H.normalizer → y ∈ H → ⁅x,y⁆ ∈ H :=
+begin
+  simp only [mem_normalizer_iff],
+  intros x y h, exact h y,
+end
+
+/-- The normalizer of a Lie subalgebra `H` is the maximal Lie subalgebra in which `H` is a Lie
+ideal. -/
+lemma le_normalizer_of_ideal {N : lie_subalgebra R L}
+  (h : ∀ (x y : L), x ∈ N → y ∈ H → ⁅x,y⁆ ∈ H) : N ≤ H.normalizer :=
+begin
+  intros x hx,
+  rw mem_normalizer_iff,
+  exact λ y, h x y hx,
+end
+
+/-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra. -/
+class is_cartan_subalgebra : Prop :=
+(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 ⊤ :=
+{ 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/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/submodule.lean

@@ -707,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 top_equiv_self_apply (x : (⊤ : lie_ideal R L)) : top_equiv_self x = x := rfl
+@[simp] lemma lie_subalgebra.top_equiv_self_apply (x : (⊤ : lie_subalgebra R L)) :
+  lie_subalgebra.top_equiv_self x = x := rfl
 
-end lie_algebra
+/-- 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 lie_ideal.top_equiv_self_apply (x : (⊤ : lie_ideal R L)) :
+  lie_ideal.top_equiv_self x = x := rfl
+
+end top_equiv_self