feat(algebra/lie/{subalgebra,submodule}): grab bag of new lemmas (#6342)

I'm splitting these off from other work to simplify subsequent reviews.
Cosmetic changes aside, the following summarises what I am proposing:

New definitions:
 - `lie_subalgebra.of_le`

Definition tweaks:
 - `lie_hom.range` [use coercion instead of `lie_hom.to_linear_map`]
 - `lie_ideal.map` [factor through `submodule.map` to avoid dropping all the way down to `set.image`]

New lemmas:
 - `lie_ideal.coe_to_lie_subalgebra_to_submodule`
 - `lie_ideal.incl_range`
 - `lie_hom.ideal_range_eq_lie_span_range`
 - `lie_hom.is_ideal_morphism_iff`
 - `lie_subalgebra.mem_range`
 - `lie_subalgebra.mem_map`
 - `lie_subalgebra.mem_of_le`
 - `lie_subalgebra.of_le_eq_comap_incl`
 - `lie_subalgebra.exists_lie_ideal_coe_eq_iff`
 - `lie_subalgebra.exists_nested_lie_ideal_coe_eq_iff`
 - `submodule.exists_lie_submodule_coe_eq_iff`
 - `lie_submodule.coe_lie_span_submodule_eq_iff`

Deleted lemma:
 - `lie_hom.range_bracket`

New simp attributes:
 - `lie_subalgebra.mem_top`
 - `lie_submodule.mem_top`

src/algebra/lie/subalgebra.lean

@@ -130,50 +130,56 @@ def lie_subalgebra.incl (L' : lie_subalgebra R L) : L' →ₗ⁅R⁆ L :=
 { map_lie' := λ x y, by { rw [linear_map.to_fun_eq_coe, submodule.subtype_apply], refl, },
   ..L'.to_submodule.subtype }
 
+namespace lie_hom
+
 /-- The range of a morphism of Lie algebras is a Lie subalgebra. -/
-def lie_hom.range : lie_subalgebra R L₂ :=
+def range : lie_subalgebra R L₂ :=
 { lie_mem' := λ x y,
     show x ∈ f.to_linear_map.range → y ∈ f.to_linear_map.range → ⁅x, y⁆ ∈ f.to_linear_map.range,
     by { repeat { rw linear_map.mem_range }, rintros ⟨x', hx⟩ ⟨y', hy⟩, refine ⟨⁅x', y'⁆, _⟩,
-         rw [←hx, ←hy], change f ⁅x', y'⁆ = ⁅f x', f y'⁆, rw lie_hom.map_lie, },
-  ..f.to_linear_map.range }
-
-@[simp] lemma lie_hom.range_bracket (x y : f.range) :
-  (↑⁅x, y⁆ : L₂) = ⁅(↑x : L₂), ↑y⁆ := rfl
+         rw [←hx, ←hy], change f ⁅x', y'⁆ = ⁅f x', f y'⁆, rw map_lie, },
+  ..(f : L →ₗ[R] L₂).range }
 
-@[simp] lemma lie_hom.range_coe : (f.range : set L₂) = set.range f :=
+@[simp] lemma range_coe : (f.range : set L₂) = set.range f :=
 linear_map.range_coe ↑f
 
+@[simp] lemma mem_range (x : L₂) : x ∈ f.range ↔ ∃ (y : L), f y = x := linear_map.mem_range
+
+end lie_hom
+
 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, }
+variables (K K' : lie_subalgebra R L) (K₂ : lie_subalgebra R L₂)
+
+@[simp] lemma incl_range : K.incl.range = K :=
+by { rw ← coe_to_submodule_eq_iff, exact (K : submodule R L).range_subtype, }
 
 /-- The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
 codomain. -/
-def map (L' : lie_subalgebra R L) : lie_subalgebra R L₂ :=
+def map : 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₂))}
+    exact ⟨⁅x', y'⁆, K.lie_mem hx' hy', f.map_lie x' y'⟩, },
+..((K : submodule R L).map (f : L →ₗ[R] L₂)) }
+
+@[simp] lemma mem_map (x : L₂) : x ∈ K.map f ↔ ∃ (y : L), y ∈ K ∧ f y = x := submodule.mem_map
 
-@[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₂) :=
+-- TODO Rename and state for homs instead of equivs.
+@[simp] lemma mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (x : L₂) :
+  x ∈ K.map (e : L →ₗ⁅R⁆ L₂) ↔ x ∈ (K : 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 :=
+def comap : 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₂)), }
+    { suffices : ⁅f x, f y⁆ ∈ K₂, by { simp [this], }, exact K₂.lie_mem hx hy, },
+  ..((K₂ : 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) :=
@@ -201,7 +207,7 @@ instance : has_top (lie_subalgebra R L) :=
 
 @[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
+@[simp] 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),
@@ -294,7 +300,7 @@ section nested_subalgebras
 variables (h : K ≤ K')
 
 /-- Given two nested Lie subalgebras `K ⊆ K'`, the inclusion `K ↪ K'` is a morphism of Lie
-algebras.-/
+algebras. -/
 def hom_of_le : K →ₗ⁅R⁆ K' :=
 { map_lie' := λ x y, rfl,
   ..submodule.of_le h }
@@ -307,6 +313,21 @@ 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]
 
+/-- Given two nested Lie subalgebras `K ⊆ K'`, we can view `K` as a Lie subalgebra of `K'`,
+regarded as Lie algebra in its own right. -/
+def of_le : lie_subalgebra R K' := (hom_of_le h).range
+
+@[simp] lemma mem_of_le (x : K') : x ∈ of_le h ↔ (x : L) ∈ K :=
+begin
+  simp only [of_le, hom_of_le_apply, lie_hom.mem_range],
+  split,
+  { rintros ⟨y, rfl⟩, exact y.property, },
+  { intros h, use ⟨(x : L), h⟩, simp, },
+end
+
+lemma of_le_eq_comap_incl : of_le h = K.comap K'.incl :=
+by { ext, rw mem_of_le, refl, }
+
 end nested_subalgebras
 
 lemma map_le_iff_le_comap {K : lie_subalgebra R L} {K' : lie_subalgebra R L₂} :
@@ -329,9 +350,7 @@ variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [li
 noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) :
   L₁ ≃ₗ⁅R⁆ f.range :=
 have h' : (f : L₁ →ₗ[R] L₂).ker = ⊥ := linear_map.ker_eq_bot_of_injective h,
-{ map_lie' := λ x y, by { apply set_coe.ext,
-    simp only [linear_equiv.of_injective_apply, lie_hom.range_bracket],
-    apply f.map_lie, },
+{ map_lie' := λ x y, by { apply set_coe.ext, simpa, },
 ..(linear_equiv.of_injective ↑f h')}
 
 @[simp] lemma of_injective_apply (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) (x : L₁) :

src/algebra/lie/submodule.lean

@@ -123,8 +123,44 @@ instance : has_coe (lie_ideal R L) (lie_subalgebra R L) := ⟨λ I, lie_ideal_su
 @[norm_cast] lemma lie_ideal.coe_to_subalgebra (I : lie_ideal R L) :
   ((I : lie_subalgebra R L) : set L) = I := rfl
 
+@[norm_cast] lemma lie_ideal.coe_to_lie_subalgebra_to_submodule (I : lie_ideal R L) :
+  ((I : lie_subalgebra R L) : submodule R L) = I := rfl
+
 end lie_ideal
 
+variables {R M}
+
+lemma submodule.exists_lie_submodule_coe_eq_iff (p : submodule R M) :
+  (∃ (N : lie_submodule R L M), ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p :=
+begin
+  split,
+  { rintros ⟨N, rfl⟩, exact N.lie_mem, },
+  { intros h, use { lie_mem := h, ..p }, exact lie_submodule.coe_to_submodule_mk p _, },
+end
+
+namespace lie_subalgebra
+
+variables {L}
+
+lemma exists_lie_ideal_coe_eq_iff (K : lie_subalgebra R L):
+  (∃ (I : lie_ideal R L), ↑I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K :=
+begin
+  simp only [← coe_to_submodule_eq_iff, lie_ideal.coe_to_lie_subalgebra_to_submodule,
+    submodule.exists_lie_submodule_coe_eq_iff L],
+  exact iff.rfl,
+end
+
+lemma exists_nested_lie_ideal_coe_eq_iff {K K' : lie_subalgebra R L} (h : K ≤ K') :
+  (∃ (I : lie_ideal R K'), ↑I = of_le h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K :=
+begin
+  simp only [exists_lie_ideal_coe_eq_iff, coe_bracket, mem_of_le],
+  split,
+  { intros h' x y hx hy, exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy, },
+  { rintros h' ⟨x, hx⟩ ⟨y, hy⟩ hy', exact h' x y hx hy', },
+end
+
+end lie_subalgebra
+
 end lie_submodule
 
 namespace lie_submodule
@@ -169,7 +205,7 @@ instance : has_top (lie_submodule R L M) :=
 
 @[simp] lemma top_coe_submodule : ((⊤ : lie_submodule R L M) : submodule R M) = ⊤ := rfl
 
-lemma mem_top (x : M) : x ∈ (⊤ : lie_submodule R L M) := mem_univ x
+@[simp] lemma mem_top (x : M) : x ∈ (⊤ : lie_submodule R L M) := mem_univ x
 
 instance : has_inf (lie_submodule R L M) :=
 ⟨λ N N', { lie_mem := λ x m h, mem_inter (N.lie_mem h.1) (N'.lie_mem h.2),
@@ -336,6 +372,14 @@ by { rw lie_span_le, exact subset.trans h subset_lie_span, }
 lemma lie_span_eq : lie_span R L (N : set M) = N :=
 le_antisymm (lie_span_le.mpr rfl.subset) subset_lie_span
 
+lemma coe_lie_span_submodule_eq_iff {p : submodule R M} :
+  (lie_span R L (p : set M) : submodule R M) = p ↔ ∃ (N : lie_submodule R L M), ↑N = p :=
+begin
+  rw p.exists_lie_submodule_coe_eq_iff L, split; intros h,
+  { intros x m hm, rw [← h, mem_coe_submodule], exact lie_mem _ (subset_lie_span hm), },
+  { rw [← coe_to_submodule_mk p h, coe_to_submodule, coe_to_submodule_eq_iff, lie_span_eq], },
+end
+
 end lie_span
 
 end lattice_structure
@@ -383,7 +427,7 @@ variables (f : L →ₗ⁅R⁆ L') (I : lie_ideal R L) (J : lie_ideal R L')
 Note that unlike `lie_submodule.map`, we must take the `lie_span` of the image. Mathematically
 this is because although `f` makes `L'` into a Lie module over `L`, in general the `L` submodules of
 `L'` are not the same as the ideals of `L'`. -/
-def map : lie_ideal R L' := lie_submodule.lie_span R L' (f '' I)
+def map : lie_ideal R L' := lie_submodule.lie_span R L' $ (I : submodule R L).map (f : L →ₗ[R] L')
 
 /-- A morphism of Lie algebras `f : L → L'` pulls back Lie ideals of `L'` to Lie ideals of `L`.
 
@@ -432,7 +476,7 @@ by { rw lie_submodule.le_def at h, apply lie_submodule.lie_span_mono (set.image_
 lemma map_of_image (h : f '' I = J) : I.map f = J :=
 begin
   apply le_antisymm,
-  { erw [lie_submodule.lie_span_le, h], },
+  { erw [lie_submodule.lie_span_le, submodule.map_coe, h], },
   { rw [lie_submodule.le_def, ← h], exact lie_submodule.subset_lie_span, },
 end
 
@@ -462,12 +506,28 @@ def ker : lie_ideal R L := lie_ideal.comap f ⊥
 /-- The range of a morphism of Lie algebras as an ideal in the codomain. -/
 def ideal_range : lie_ideal R L' := lie_ideal.map f ⊤
 
+lemma ideal_range_eq_lie_span_range :
+  f.ideal_range = lie_submodule.lie_span R L' f.range := rfl
+
 /-- The condition that the image of a morphism of Lie algebras is an ideal. -/
 def is_ideal_morphism : Prop := (f.ideal_range : lie_subalgebra R L') = f.range
 
 @[simp] lemma is_ideal_morphism_def :
   f.is_ideal_morphism ↔ (f.ideal_range : lie_subalgebra R L') = f.range := iff.rfl
 
+lemma is_ideal_morphism_iff :
+  f.is_ideal_morphism ↔ ∀ (x : L') (y : L), ∃ (z : L), ⁅x, f y⁆ = f z :=
+begin
+  simp only [is_ideal_morphism_def, ideal_range_eq_lie_span_range,
+    ← lie_subalgebra.coe_to_submodule_eq_iff, ← f.range.coe_to_submodule,
+    lie_ideal.coe_to_lie_subalgebra_to_submodule, lie_submodule.coe_lie_span_submodule_eq_iff,
+    lie_subalgebra.mem_coe_submodule, mem_range, exists_imp_distrib,
+    submodule.exists_lie_submodule_coe_eq_iff],
+  split,
+  { intros h x y, obtain ⟨z, hz⟩ := h x (f y) y rfl, use z, exact hz.symm, },
+  { intros h x y z hz, obtain ⟨w, hw⟩ := h x z, use w, rw [← hw, hz], },
+end
+
 lemma range_subset_ideal_range : (f.range : set L') ⊆ f.ideal_range := lie_submodule.subset_lie_span
 
 lemma map_le_ideal_range : I.map f ≤ f.ideal_range := lie_ideal.map_mono le_top
@@ -540,7 +600,7 @@ begin
   apply lie_submodule.lie_span_mono,
   rintros x ⟨y, hy₁, hy₂⟩, rw ← hy₂,
   erw lie_submodule.mem_sup at hy₁, obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁, rw ← hy,
-  rw [f.map_add, f.mem_ker.mp hz₂, add_zero], exact ⟨z₁, hz₁, rfl⟩,
+  rw [f.coe_to_linear_map, f.map_add, f.mem_ker.mp hz₂, add_zero], exact ⟨z₁, hz₁, rfl⟩,
 end
 
 @[simp] lemma map_comap_eq (h : f.is_ideal_morphism) : map f (comap f J) = f.ideal_range ⊓ J :=
@@ -562,6 +622,8 @@ variables (f I J)
 of Lie algebras. -/
 def incl : I →ₗ⁅R⁆ L := (I : lie_subalgebra R L).incl
 
+@[simp] lemma incl_range : I.incl.range = I := (I : lie_subalgebra R L).incl_range
+
 @[simp] lemma incl_apply (x : I) : I.incl x = x := rfl
 
 @[simp] lemma incl_coe : (I.incl : I →ₗ[R] L) = (I : submodule R L).subtype := rfl
@@ -575,18 +637,16 @@ by rw [← lie_submodule.coe_to_submodule_eq_iff, I.incl.ker_coe_submodule,
 
 @[simp] lemma incl_ideal_range : I.incl.ideal_range = I :=
 begin
-  apply le_antisymm,
-  { erw lie_submodule.lie_span_le, intros x hx,
-    simp only [true_and, set.mem_image, incl_apply, set.mem_univ, lie_submodule.top_coe] at hx,
-    obtain ⟨y, hy⟩ := hx, rw ← hy, exact y.property, },
-  { rw [lie_submodule.le_def, ← lie_ideal.coe_to_subalgebra, ← (I : lie_subalgebra R L).range_incl],
-    exact I.incl.range_subset_ideal_range, },
+  rw [lie_hom.ideal_range_eq_lie_span_range, ← lie_subalgebra.coe_to_submodule,
+    ← lie_submodule.coe_to_submodule_eq_iff, incl_range, coe_to_lie_subalgebra_to_submodule,
+    lie_submodule.coe_lie_span_submodule_eq_iff],
+  use I,
 end
 
 lemma incl_is_ideal_morphism : I.incl.is_ideal_morphism :=
 begin
   rw [I.incl.is_ideal_morphism_def, incl_ideal_range],
-  exact (I : lie_subalgebra R L).range_incl.symm,
+  exact (I : lie_subalgebra R L).incl_range.symm,
 end
 
 end lie_ideal