feat(algebra/lie/subalgebra): define lattice structure for Lie subalg…

…ebras (#6279)

We already have the lattice structure for Lie submodules but not for subalgebras.
This is mostly a lightly-edited copy-paste of the corresponding subset of results
for Lie submodules that remain true for subalgebras.

The results which hold for Lie submodules but not for Lie subalgebras are:
  - `sup_coe_to_submodule` and `mem_sup`
  - `is_modular_lattice`

I have also made a few tweaks to bring the structure and naming of Lie
subalgebras a little closer to that of Lie submodules.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/lie/abelian.lean

@@ -187,7 +187,7 @@ end
 
 lemma lie_submodule.lie_abelian_iff_lie_self_eq_bot : is_lie_abelian I ↔ ⁅I, I⁆ = ⊥ :=
 begin
-  simp only [_root_.eq_bot_iff, lie_ideal_oper_eq_span, lie_span_le, bot_coe,
+  simp only [_root_.eq_bot_iff, lie_ideal_oper_eq_span, lie_span_le, lie_submodule.bot_coe,
     set.subset_singleton_iff, set.mem_set_of_eq, exists_imp_distrib],
   split; intros h,
   { intros z x y hz, rw [← hz, ← coe_bracket, coe_zero_iff_zero], apply h.trivial, },

src/algebra/lie/subalgebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import algebra.lie.basic
+import ring_theory.noetherian
 
 /-!
 # Lie subalgebras
@@ -48,12 +49,9 @@ instance : has_zero (lie_subalgebra R L) :=
    ..(0 : submodule R L) }⟩
 
 instance : inhabited (lie_subalgebra R L) := ⟨0⟩
-instance : has_coe (lie_subalgebra R L) (set L) := ⟨lie_subalgebra.carrier⟩
+instance : has_coe (lie_subalgebra R L) (submodule R L) := ⟨lie_subalgebra.to_submodule⟩
 instance : has_mem L (lie_subalgebra R L) := ⟨λ x L', x ∈ (L' : set L)⟩
 
-instance lie_subalgebra_coe_submodule : has_coe (lie_subalgebra R L) (submodule R L) :=
-⟨lie_subalgebra.to_submodule⟩
-
 /-- A Lie subalgebra forms a new Lie ring. -/
 instance lie_subalgebra_lie_ring (L' : lie_subalgebra R L) : lie_ring L' :=
 { bracket      := λ x y, ⟨⁅x.val, y.val⁆, L'.lie_mem' x.property y.property⟩,
@@ -79,9 +77,11 @@ lemma add_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (x + y : L) ∈ L' :=
 
 lemma lie_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (⁅x, y⁆ : L) ∈ L' := L'.lie_mem' hx hy
 
-@[simp] lemma mem_coe {x : L} : x ∈ (L' : set L) ↔ x ∈ L' := iff.rfl
+@[simp] lemma mem_carrier {x : L} : x ∈ L'.carrier ↔ x ∈ (L' : set L) := iff.rfl
+
+@[simp] lemma mem_coe_submodule {x : L} : x ∈ (L' : submodule R L) ↔ x ∈ L' := iff.rfl
 
-@[simp] lemma mem_coe' {x : L} : x ∈ (L' : submodule R L) ↔ x ∈ L' := iff.rfl
+lemma mem_coe {x : L} : x ∈ (L' : set L) ↔ x ∈ L' := iff.rfl
 
 @[simp, norm_cast] lemma coe_bracket (x y : L') : (↑⁅x, y⁆ : L) = ⁅(↑x : L), ↑y⁆ := rfl
 
@@ -99,20 +99,27 @@ lemma ext_iff' (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x 
 @[simp] lemma mk_coe (S : set L) (h₁ h₂ h₃ h₄) :
   ((⟨S, h₁, h₂, h₃, h₄⟩ : lie_subalgebra R L) : set L) = S := rfl
 
+@[simp] lemma coe_to_submodule_mk (p : submodule R L) (h) :
+  (({lie_mem' := h, ..p} : lie_subalgebra R L) : submodule R L) = p :=
+by { cases p, refl, }
+
 lemma coe_injective : function.injective (coe : lie_subalgebra R L → set L) :=
 λ L₁' L₂' h, by cases L₁'; cases L₂'; congr'
 
-@[simp, norm_cast] theorem coe_set_eq (L₁' L₂' : lie_subalgebra R L) :
+@[norm_cast] theorem coe_set_eq (L₁' L₂' : lie_subalgebra R L) :
   (L₁' : set L) = L₂' ↔ L₁' = L₂' := coe_injective.eq_iff
 
 lemma to_submodule_injective :
   function.injective (coe : lie_subalgebra R L → submodule R L) :=
 λ L₁' L₂' h, by { rw submodule.ext'_iff at h, rw ← coe_set_eq, exact h, }
 
-@[simp] lemma coe_to_submodule_eq (L₁' L₂' : lie_subalgebra R L) :
+@[simp] lemma coe_to_submodule_eq_iff (L₁' L₂' : lie_subalgebra R L) :
   (L₁' : submodule R L) = (L₂' : submodule R L) ↔ L₁' = L₂' :=
 to_submodule_injective.eq_iff
 
+@[norm_cast]
+lemma coe_to_submodule : ((L' : submodule R L) : set L) = L' := rfl
+
 end lie_subalgebra
 
 variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂]
@@ -137,23 +144,180 @@ def lie_hom.range : lie_subalgebra R L₂ :=
 @[simp] lemma lie_hom.range_coe : (f.range : set L₂) = set.range f :=
 linear_map.range_coe ↑f
 
-@[simp] lemma lie_subalgebra.range_incl (L' : lie_subalgebra R L) : L'.incl.range = L' :=
-by { rw ← lie_subalgebra.coe_to_submodule_eq, exact (L' : submodule R L).range_subtype, }
+namespace lie_subalgebra
+
+@[simp] lemma range_incl (L' : lie_subalgebra R L) : L'.incl.range = L' :=
+by { rw ← coe_to_submodule_eq_iff, exact (L' : submodule R L).range_subtype, }
 
 /-- The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
 codomain. -/
-def lie_subalgebra.map (L' : lie_subalgebra R L) : lie_subalgebra R L₂ :=
+def map (L' : lie_subalgebra R L) : lie_subalgebra R L₂ :=
 { lie_mem' := λ x y hx hy, by {
     erw submodule.mem_map at hx, rcases hx with ⟨x', hx', hx⟩, rw ←hx,
     erw submodule.mem_map at hy, rcases hy with ⟨y', hy', hy⟩, rw ←hy,
     erw submodule.mem_map,
     exact ⟨⁅x', y'⁆, L'.lie_mem hx' hy', lie_hom.map_lie f x' y'⟩, },
 ..((L' : submodule R L).map (f : L →ₗ[R] L₂))}
 
-@[simp] lemma lie_subalgebra.mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (L' : lie_subalgebra R L) (x : L₂) :
+@[simp] lemma mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (L' : lie_subalgebra R L) (x : L₂) :
   x ∈ L'.map (e : L →ₗ⁅R⁆ L₂) ↔ x ∈ (L' : submodule R L).map (e : L →ₗ[R] L₂) :=
 iff.rfl
 
+/-- The preimage of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
+domain. -/
+def comap (L' : lie_subalgebra R L₂) : lie_subalgebra R L :=
+{ lie_mem' := λ x y hx hy, by
+    { suffices : ⁅f x, f y⁆ ∈ L', by { simp [this], }, exact L'.lie_mem hx hy, },
+  ..((L' : submodule R L₂).comap (f : L →ₗ[R] L₂)), }
+
+section lattice_structure
+
+variables (K K' : lie_subalgebra R L)
+
+open set
+
+instance : partial_order (lie_subalgebra R L) :=
+{ le := λ N N', ∀ ⦃x⦄, x ∈ N → x ∈ N', -- Overriding `le` like this gives a better defeq.
+  ..partial_order.lift (coe : lie_subalgebra R L → set L) coe_injective }
+
+lemma le_def : K ≤ K' ↔ (K : set L) ⊆ K' := iff.rfl
+
+@[simp, norm_cast] lemma coe_submodule_le_coe_submodule : (K : submodule R L) ≤ K' ↔ K ≤ K' :=
+iff.rfl
+
+instance : has_bot (lie_subalgebra R L) := ⟨0⟩
+
+@[simp] lemma bot_coe : ((⊥ : lie_subalgebra R L) : set L) = {0} := rfl
+
+@[simp] lemma bot_coe_submodule : ((⊥ : lie_subalgebra R L) : submodule R L) = ⊥ := rfl
+
+@[simp] lemma mem_bot (x : L) : x ∈ (⊥ : lie_subalgebra R L) ↔ x = 0 := mem_singleton_iff
+
+instance : has_top (lie_subalgebra R L) :=
+⟨{ lie_mem' := λ x y hx hy, mem_univ ⁅x, y⁆,
+   ..(⊤ : submodule R L) }⟩
+
+@[simp] lemma top_coe : ((⊤ : lie_subalgebra R L) : set L) = univ := rfl
+
+@[simp] lemma top_coe_submodule : ((⊤ : lie_subalgebra R L) : submodule R L) = ⊤ := rfl
+
+lemma mem_top (x : L) : x ∈ (⊤ : lie_subalgebra R L) := mem_univ x
+
+instance : has_inf (lie_subalgebra R L) :=
+⟨λ K K', { lie_mem' := λ x y hx hy, mem_inter (K.lie_mem hx.1 hy.1) (K'.lie_mem hx.2 hy.2),
+            ..(K ⊓ K' : submodule R L) }⟩
+
+instance : has_Inf (lie_subalgebra R L) :=
+⟨λ S, { lie_mem' := λ x y hx hy, by
+        { simp only [submodule.mem_carrier, mem_Inter, submodule.Inf_coe, mem_set_of_eq,
+            forall_apply_eq_imp_iff₂, exists_imp_distrib] at *,
+          intros K hK, exact K.lie_mem (hx K hK) (hy K hK), },
+        ..Inf {(s : submodule R L) | s ∈ S} }⟩
+
+@[simp] theorem inf_coe : (↑(K ⊓ K') : set L) = K ∩ K' := rfl
+
+@[simp] lemma Inf_coe_to_submodule (S : set (lie_subalgebra R L)) :
+  (↑(Inf S) : submodule R L) = Inf {(s : submodule R L) | s ∈ S} := rfl
+
+@[simp] lemma Inf_coe (S : set (lie_subalgebra R L)) : (↑(Inf S) : set L) = ⋂ s ∈ S, (s : set L) :=
+begin
+  rw [← coe_to_submodule, Inf_coe_to_submodule, submodule.Inf_coe],
+  ext x,
+  simpa only [mem_Inter, mem_set_of_eq, forall_apply_eq_imp_iff₂, exists_imp_distrib],
+end
+
+lemma Inf_glb (S : set (lie_subalgebra R L)) : is_glb S (Inf S) :=
+begin
+  have h : ∀ (K K' : lie_subalgebra R L), (K : set L) ≤ K' ↔ K ≤ K', { intros, exact iff.rfl, },
+  simp only [is_glb.of_image h, Inf_coe, is_glb_binfi],
+end
+
+/-- The set of Lie subalgebras of a Lie algebra form a complete lattice.
+
+We provide explicit values for the fields `bot`, `top`, `inf` to get more convenient definitions
+than we would otherwise obtain from `complete_lattice_of_Inf`. -/
+instance : complete_lattice (lie_subalgebra R L) :=
+{ bot          := ⊥,
+  bot_le       := λ N _ h, by { rw mem_bot at h, rw h, exact N.zero_mem', },
+  top          := ⊤,
+  le_top       := λ _ _ _, trivial,
+  inf          := (⊓),
+  le_inf       := λ N₁ N₂ N₃ h₁₂ h₁₃ m hm, ⟨h₁₂ hm, h₁₃ hm⟩,
+  inf_le_left  := λ _ _ _, and.left,
+  inf_le_right := λ _ _ _, and.right,
+  ..complete_lattice_of_Inf _ Inf_glb }
+
+instance : add_comm_monoid (lie_subalgebra R L) :=
+{ add       := (⊔),
+  add_assoc := λ _ _ _, sup_assoc,
+  zero      := ⊥,
+  zero_add  := λ _, bot_sup_eq,
+  add_zero  := λ _, sup_bot_eq,
+  add_comm  := λ _ _, sup_comm, }
+
+@[simp] lemma add_eq_sup : K + K' = K ⊔ K' := rfl
+
+@[norm_cast, simp] lemma inf_coe_to_submodule :
+  (↑(K ⊓ K') : submodule R L) = (K : submodule R L) ⊓ (K' : submodule R L) := rfl
+
+@[simp] lemma mem_inf (x : L) : x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K' :=
+by rw [← mem_coe_submodule, ← mem_coe_submodule, ← mem_coe_submodule, inf_coe_to_submodule,
+  submodule.mem_inf]
+
+lemma eq_bot_iff : K = ⊥ ↔ ∀ (x : L), x ∈ K → x = 0 :=
+by { rw eq_bot_iff, exact iff.rfl, }
+
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma subsingleton_of_bot : subsingleton (lie_subalgebra R ↥(⊥ : lie_subalgebra R L)) :=
+begin
+  apply subsingleton_of_bot_eq_top,
+  ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw submodule.mem_bot at hx, subst hx,
+  simp only [true_iff, eq_self_iff_true, submodule.mk_eq_zero, mem_bot],
+end
+
+variables (R L)
+
+lemma well_founded_of_noetherian [is_noetherian R L] :
+  well_founded ((>) : lie_subalgebra R L → lie_subalgebra R L → Prop) :=
+begin
+  let f : ((>) : lie_subalgebra R L → lie_subalgebra R L → Prop) →r
+          ((>) : submodule R L → submodule R L → Prop) :=
+  { to_fun       := coe,
+    map_rel' := λ N N' h, h, },
+  apply f.well_founded, rw ← is_noetherian_iff_well_founded, apply_instance,
+end
+
+variables {R L K K' f}
+
+section nested_subalgebras
+
+variables (h : K ≤ K')
+
+/-- Given two nested Lie subalgebras `K ⊆ K'`, the inclusion `K ↪ K'` is a morphism of Lie
+algebras.-/
+def hom_of_le : K →ₗ⁅R⁆ K' :=
+{ map_lie' := λ x y, rfl,
+  ..submodule.of_le h }
+
+@[simp] lemma coe_hom_of_le (x : K) : (hom_of_le h x : L) = x := rfl
+
+lemma hom_of_le_apply (x : K) : hom_of_le h x = ⟨x.1, h x.2⟩ := rfl
+
+lemma hom_of_le_injective : function.injective (hom_of_le h) :=
+λ x y, by simp only [hom_of_le_apply, imp_self, subtype.mk_eq_mk, submodule.coe_eq_coe,
+  subtype.val_eq_coe]
+
+end nested_subalgebras
+
+lemma map_le_iff_le_comap {K : lie_subalgebra R L} {K' : lie_subalgebra R L₂} :
+  map f K ≤ K' ↔ K ≤ comap f K' := set.image_subset_iff
+
+lemma gc_map_comap : galois_connection (map f) (comap f) := λ K K', map_le_iff_le_comap
+
+end lattice_structure
+
+end lie_subalgebra
+
 end lie_subalgebra
 
 namespace lie_equiv