feat(algebra/lie/weights): define product of root vectors and weight …

…vectors (#7591)

Also some related results, most notably that the zero root space is a subalgebra.

src/algebra/lie/abelian.lean

@@ -266,7 +266,7 @@ begin
   simp only [_root_.eq_bot_iff, lie_ideal_oper_eq_span, lie_submodule.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, },
+  { intros z x y hz, rw [← hz, ← lie_subalgebra.coe_bracket, coe_zero_iff_zero], apply h.trivial, },
   { exact ⟨λ x y, by { rw ← coe_zero_iff_zero, apply h _ x y, refl, }⟩, },
 end
 

src/algebra/lie/subalgebra.lean

@@ -126,6 +126,7 @@ lemma coe_to_submodule : ((L' : submodule R L) : set L) = L' := rfl
 section lie_module
 
 variables {M : Type w} [add_comm_group M] [lie_ring_module L M]
+variables {N : Type w₁} [add_comm_group N] [lie_ring_module L N] [module R N] [lie_module R L N]
 
 /-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie ring module
 `M` of `L`, we may regard `M` as a Lie ring module of `L'` by restriction. -/
@@ -137,12 +138,24 @@ instance : lie_ring_module L' M :=
 
 @[simp] lemma coe_bracket_of_module (x : L') (m : M) : ⁅x, m⁆ = ⁅(x : L), m⁆ := rfl
 
+variables [module R M] [lie_module R L M]
+
 /-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie module `M` of
 `L`, we may regard `M` as a Lie module of `L'` by restriction. -/
-instance [module R M] [lie_module R L M] : lie_module R L' M :=
+instance : lie_module R L' M :=
 { smul_lie := λ t x m, by simp only [coe_bracket_of_module, smul_lie, submodule.coe_smul_of_tower],
   lie_smul := λ t x m, by simp only [coe_bracket_of_module, lie_smul], }
 
+/-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra
+`L' ⊆ L`. -/
+def _root_.lie_module_hom.restrict_lie (f : M →ₗ⁅R,L⁆ N) (L' : lie_subalgebra R L) : M →ₗ⁅R,L'⁆ N :=
+{ map_lie' := λ x m, f.map_lie ↑x m,
+  .. (f : M →ₗ[R] N)}
+
+@[simp] lemma _root_.lie_module_hom.coe_restrict_lie (f : M →ₗ⁅R,L⁆ N) :
+  ⇑(f.restrict_lie L') = f :=
+rfl
+
 end lie_module
 
 /-- The embedding of a Lie subalgebra into the ambient space as a morphism of Lie algebras. -/

src/algebra/lie/submodule.lean

@@ -112,6 +112,18 @@ instance : lie_module R L N :=
 { lie_smul := by { intros t x y, apply set_coe.ext, apply lie_smul, },
   smul_lie := by { intros t x y, apply set_coe.ext, apply smul_lie, }, }
 
+@[simp, norm_cast] lemma coe_zero : ((0 : N) : M) = (0 : M) := rfl
+
+@[simp, norm_cast] lemma coe_add (m m' : N) : (↑(m + m') : M) = (m : M) + (m' : M) := rfl
+
+@[simp, norm_cast] lemma coe_neg (m : N) : (↑(-m) : M) = -(m : M) := rfl
+
+@[simp, norm_cast] lemma coe_sub (m m' : N) : (↑(m - m') : M) = (m : M) - (m' : M) := rfl
+
+@[simp, norm_cast] lemma coe_smul (t : R) (m : N) : (↑(t • m) : M) = t • (m : M) := rfl
+
+@[simp, norm_cast] lemma coe_bracket (x : L) (m : N) : (↑⁅x, m⁆ : M) = ⁅x, ↑m⁆ := rfl
+
 end lie_submodule
 
 section lie_ideal
@@ -155,7 +167,21 @@ namespace lie_subalgebra
 
 variables {L}
 
-lemma exists_lie_ideal_coe_eq_iff (K : lie_subalgebra R L):
+/-- Given a Lie subalgebra `K ⊆ L`, if we view `L` as a `K`-module by restriction, it contains
+a distinguished Lie submodule for the action of `K`, namely `K` itself. -/
+def to_lie_submodule (K : lie_subalgebra R L) : lie_submodule R K L :=
+{ lie_mem := λ x y hy, K.lie_mem x.property hy,
+  .. (K : submodule R L) }
+
+@[simp] lemma coe_to_lie_submodule (K : lie_subalgebra R L) :
+  (K.to_lie_submodule : submodule R L) = K :=
+rfl
+
+@[simp] lemma mem_to_lie_submodule {K : lie_subalgebra R L} (x : L) :
+  x ∈ K.to_lie_submodule ↔ x ∈ K :=
+iff.rfl
+
+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,

src/algebra/lie/weights.lean

@@ -30,6 +30,8 @@ Basic definitions and properties of the above ideas are provided in this file.
   * `lie_module.is_weight`
   * `lie_algebra.root_space`
   * `lie_algebra.is_root`
+  * `lie_algebra.root_space_weight_space_product`
+  * `lie_algebra.root_space_product`
 
 ## References
 
@@ -67,8 +69,10 @@ lemma mem_pre_weight_space (χ : L → R) (m : M) :
   m ∈ pre_weight_space M χ ↔ ∀ x, ∃ (k : ℕ), ((to_endomorphism R L M x - (χ x) • 1)^k) m = 0 :=
 by simp [pre_weight_space, -linear_map.pow_apply]
 
+variables (L)
+
 /-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii). -/
-private lemma weight_vector_multiplication (M₁ : Type w₁) (M₂ : Type w₂) (M₃ : Type w₃)
+protected lemma weight_vector_multiplication (M₁ : Type w₁) (M₂ : Type w₂) (M₃ : Type w₃)
   [add_comm_group M₁] [module R M₁] [lie_ring_module L M₁] [lie_module R L M₁]
   [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂]
   [add_comm_group M₃] [module R M₃] [lie_ring_module L M₃] [lie_module R L M₃]
@@ -153,13 +157,13 @@ begin
   { rw [linear_map.mul_apply, linear_map.pow_map_zero_of_le hj hf₂, linear_map.map_zero], },
 end
 
-variables {M}
+variables {L M}
 
 lemma lie_mem_pre_weight_space_of_mem_pre_weight_space {χ₁ χ₂ : L → R} {x : L} {m : M}
   (hx : x ∈ pre_weight_space L χ₁) (hm : m ∈ pre_weight_space M χ₂) :
   ⁅x, m⁆ ∈ pre_weight_space M (χ₁ + χ₂) :=
 begin
-  apply weight_vector_multiplication L M M (to_module_hom R L M) χ₁ χ₂,
+  apply lie_module.weight_vector_multiplication L L M M (to_module_hom R L M) χ₁ χ₂,
   simp only [lie_module_hom.coe_to_linear_map, function.comp_app, linear_map.coe_comp,
     tensor_product.map_incl, linear_map.mem_range],
   use [⟨x, hx⟩ ⊗ₜ ⟨m, hm⟩],
@@ -231,37 +235,144 @@ end lie_module
 
 namespace lie_algebra
 
+open_locale tensor_product
+open tensor_product.lie_module
+open lie_module
+
 /-- Given a nilpotent Lie subalgebra `H ⊆ L`, the root space of a map `χ : H → R` is the weight
 space of `L` regarded as a module of `H` via the adjoint action. -/
-abbreviation root_space (χ : H → R) : lie_submodule R H L := lie_module.weight_space L χ
+abbreviation root_space (χ : H → R) : lie_submodule R H L := weight_space L χ
 
 @[simp] lemma zero_root_space_eq_top_of_nilpotent [h : is_nilpotent R L] :
   root_space (⊤ : lie_subalgebra R L) 0 = ⊤ :=
-lie_module.zero_weight_space_eq_top_of_nilpotent L
+zero_weight_space_eq_top_of_nilpotent L
 
 /-- A root of a Lie algebra `L` with respect to a nilpotent subalgebra `H ⊆ L` is a weight of `L`,
 regarded as a module of `H` via the adjoint action. -/
-abbreviation is_root := lie_module.is_weight H L
+abbreviation is_root := is_weight H L
 
 @[simp] lemma root_space_comap_eq_weight_space (χ : H → R) :
-  (root_space H χ).comap H.incl' = lie_module.weight_space H χ :=
+  (root_space H χ).comap H.incl' = weight_space H χ :=
 begin
   ext x,
-  let f : H → module.End R L := λ y, lie_module.to_endomorphism R H L y - (χ y) • 1,
-  let g : H → module.End R H := λ y, lie_module.to_endomorphism R H H y - (χ y) • 1,
+  let f : H → module.End R L := λ y, to_endomorphism R H L y - (χ y) • 1,
+  let g : H → module.End R H := λ y, to_endomorphism R H H y - (χ y) • 1,
   suffices : (∀ (y : H), ∃ (k : ℕ), ((f y)^k).comp (H.incl : H →ₗ[R] L) x = 0) ↔
               ∀ (y : H), ∃ (k : ℕ), (H.incl : H →ₗ[R] L).comp ((g y)^k) x = 0,
   { simp only [lie_hom.coe_to_linear_map, lie_subalgebra.coe_incl, function.comp_app,
       linear_map.coe_comp, submodule.coe_eq_zero] at this,
-    simp only [lie_module.mem_weight_space, lie_module.mem_pre_weight_space,
+    simp only [mem_weight_space, mem_pre_weight_space,
       lie_subalgebra.coe_incl', lie_submodule.mem_comap, this], },
   have hfg : ∀ (y : H), (f y).comp (H.incl : H →ₗ[R] L) = (H.incl : H →ₗ[R] L).comp (g y),
   { rintros ⟨y, hz⟩, ext ⟨z, hz⟩,
-    simp only [submodule.coe_sub, lie_module.to_endomorphism_apply_apply, lie_hom.coe_to_linear_map,
+    simp only [submodule.coe_sub, to_endomorphism_apply_apply, lie_hom.coe_to_linear_map,
       linear_map.one_apply, lie_subalgebra.coe_incl, lie_subalgebra.coe_bracket_of_module,
       lie_subalgebra.coe_bracket, linear_map.smul_apply, function.comp_app,
       submodule.coe_smul_of_tower, linear_map.coe_comp, linear_map.sub_apply], },
   simp_rw [linear_map.commute_pow_left_of_commute (hfg _)],
 end
 
+variables {H M}
+
+lemma lie_mem_weight_space_of_mem_weight_space {χ₁ χ₂ : H → R} {x : L} {m : M}
+  (hx : x ∈ root_space H χ₁) (hm : m ∈ weight_space M χ₂) : ⁅x, m⁆ ∈ weight_space M (χ₁ + χ₂) :=
+begin
+  apply lie_module.weight_vector_multiplication
+    H L M M ((to_module_hom R L M).restrict_lie H) χ₁ χ₂,
+  simp only [lie_module_hom.coe_to_linear_map, function.comp_app, linear_map.coe_comp,
+    tensor_product.map_incl, linear_map.mem_range],
+  use [⟨x, hx⟩ ⊗ₜ ⟨m, hm⟩],
+  simp only [submodule.subtype_apply, to_module_hom_apply, submodule.coe_mk,
+    lie_module_hom.coe_restrict_lie, tensor_product.map_tmul],
+end
+
+variables (R L H M)
+
+/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
+`R`-bilinear product of root vectors and weight vectors, compatible with the actions of `H`. -/
+def root_space_weight_space_product (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) :
+  (root_space H χ₁) ⊗[R] (weight_space M χ₂) →ₗ⁅R,H⁆ weight_space M χ₃ :=
+lift_lie R H (root_space H χ₁) (weight_space M χ₂) (weight_space M χ₃)
+{ to_fun    := λ x,
+  { to_fun    :=
+      λ m, ⟨⁅(x : L), (m : M)⁆,
+            hχ ▸ (lie_mem_weight_space_of_mem_weight_space x.property m.property) ⟩,
+    map_add'  := λ m n, by { simp only [lie_submodule.coe_add, lie_add], refl, },
+    map_smul' := λ t m, by { conv_lhs { congr, rw [lie_submodule.coe_smul, lie_smul], }, refl, }, },
+  map_add'  := λ x y, by ext m; rw [linear_map.add_apply, linear_map.coe_mk, linear_map.coe_mk,
+    linear_map.coe_mk, subtype.coe_mk, lie_submodule.coe_add, lie_submodule.coe_add, add_lie,
+    subtype.coe_mk, subtype.coe_mk],
+  map_smul' := λ t x, by ext m; rw [linear_map.smul_apply, linear_map.coe_mk, linear_map.coe_mk,
+    subtype.coe_mk, lie_submodule.coe_smul, smul_lie, lie_submodule.coe_smul, subtype.coe_mk],
+  map_lie'  := λ x y, by ext m; rw [lie_hom.lie_apply, lie_submodule.coe_sub, linear_map.coe_mk,
+    linear_map.coe_mk, subtype.coe_mk, subtype.coe_mk, lie_submodule.coe_bracket,
+    lie_submodule.coe_bracket, subtype.coe_mk, lie_subalgebra.coe_bracket_of_module,
+    lie_subalgebra.coe_bracket_of_module, lie_submodule.coe_bracket,
+    lie_subalgebra.coe_bracket_of_module, lie_lie], }
+
+@[simp] lemma coe_root_space_weight_space_product_tmul
+  (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : root_space H χ₁) (m : weight_space M χ₂) :
+  (root_space_weight_space_product R L H M χ₁ χ₂ χ₃ hχ (x ⊗ₜ m) : M) = ⁅(x : L), (m : M)⁆ :=
+by simp only [root_space_weight_space_product, lift_apply, lie_module_hom.coe_to_linear_map,
+  coe_lift_lie_eq_lift_coe, submodule.coe_mk, linear_map.coe_mk, lie_module_hom.coe_mk]
+
+/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
+`R`-bilinear product of root vectors, compatible with the actions of `H`. -/
+def root_space_product (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) :
+  (root_space H χ₁) ⊗[R] (root_space H χ₂) →ₗ⁅R,H⁆ root_space H χ₃ :=
+root_space_weight_space_product R L H L χ₁ χ₂ χ₃ hχ
+
+@[simp] lemma root_space_product_def :
+  root_space_product R L H = root_space_weight_space_product R L H L :=
+rfl
+
+lemma root_space_product_tmul
+  (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : root_space H χ₁) (y : root_space H χ₂) :
+  (root_space_product R L H χ₁ χ₂ χ₃ hχ (x ⊗ₜ y) : L) = ⁅(x : L), (y : L)⁆ :=
+by simp only [root_space_product_def, coe_root_space_weight_space_product_tmul]
+
+/-- Given a nilpotent Lie subalgebra `H ⊆ L`, the root space of the zero map `0 : H → R` is a Lie
+subalgebra of `L`. -/
+def zero_root_subalgebra : lie_subalgebra R L :=
+{ lie_mem' := λ x y hx hy, by
+  { let xy : (root_space H 0) ⊗[R] (root_space H 0) := ⟨x, hx⟩ ⊗ₜ ⟨y, hy⟩,
+    suffices : (root_space_product R L H 0 0 0 (add_zero 0) xy : L) ∈ root_space H 0,
+    { rwa [root_space_product_tmul, subtype.coe_mk, subtype.coe_mk] at this, },
+    exact (root_space_product R L H 0 0 0 (add_zero 0) xy).property, },
+  .. (root_space H 0 : submodule R L) }
+
+@[simp] lemma coe_zero_root_subalgebra :
+  (zero_root_subalgebra R L H : submodule R L) = root_space H 0 :=
+rfl
+
+lemma to_lie_submodule_le_root_space_zero : H.to_lie_submodule ≤ root_space H 0 :=
+begin
+  intros x hx,
+  simp only [lie_subalgebra.mem_to_lie_submodule] at hx,
+  simp only [mem_weight_space, mem_pre_weight_space, pi.zero_apply, sub_zero, zero_smul],
+  intros y,
+  unfreezingI { obtain ⟨k, hk⟩ := (infer_instance : is_nilpotent R H) },
+  use k,
+  let f : module.End R H := to_endomorphism R H H y,
+  let g : module.End R L := to_endomorphism R H L y,
+  have hfg : g.comp (H : submodule R L).subtype = (H : submodule R L).subtype.comp f,
+  { ext z, simp only [to_endomorphism_apply_apply, submodule.subtype_apply,
+      lie_subalgebra.coe_bracket_of_module, lie_subalgebra.coe_bracket, function.comp_app,
+      linear_map.coe_comp], },
+  change (g^k).comp (H : submodule R L).subtype ⟨x, hx⟩ = 0,
+  rw linear_map.commute_pow_left_of_commute hfg k,
+  have h := iterate_to_endomorphism_mem_lower_central_series R H H y ⟨x, hx⟩ k,
+  rw [hk, lie_submodule.mem_bot] at h,
+  simp only [submodule.subtype_apply, function.comp_app, linear_map.pow_apply, linear_map.coe_comp,
+    submodule.coe_eq_zero],
+  exact h,
+end
+
+lemma le_zero_root_subalgebra : H ≤ zero_root_subalgebra R L H :=
+begin
+  rw [← lie_subalgebra.coe_submodule_le_coe_submodule, ← H.coe_to_lie_submodule,
+    coe_zero_root_subalgebra, lie_submodule.coe_submodule_le_coe_submodule],
+  exact to_lie_submodule_le_root_space_zero R L H,
+end
+
 end lie_algebra