feat(algebra/lie/subalgebra): define the restriction of a Lie module …

…to a Lie subalgebra (#7036)

src/algebra/lie/abelian.lean

@@ -83,7 +83,8 @@ lemma lie_algebra.is_lie_abelian_bot (R : Type u) (L : Type v)
   [comm_ring R] [lie_ring L] [lie_algebra R L] : is_lie_abelian (⊥ : lie_ideal R L) :=
 ⟨begin
   rintros ⟨x, hx⟩ ⟨y, hy⟩,
-  suffices : ⁅x, y⁆ = 0, { ext, simp [this], },
+  suffices : ⁅x, y⁆ = 0,
+  { ext, simp only [this, lie_subalgebra.coe_bracket, submodule.coe_mk, submodule.coe_zero], },
   change x ∈ (⊥ : lie_ideal R L) at hx, rw lie_submodule.mem_bot at hx, rw [hx, zero_lie],
 end⟩
 

src/algebra/lie/subalgebra.lean

@@ -123,6 +123,28 @@ to_submodule_injective.eq_iff
 @[norm_cast]
 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]
+
+/-- 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. -/
+instance : lie_ring_module L' M :=
+{ bracket     := λ x m, ⁅(x : L), m⁆,
+  add_lie     := λ x y m, add_lie x y m,
+  lie_add     := λ x y m, lie_add x y m,
+  leibniz_lie := λ x y m, leibniz_lie x y m, }
+
+@[simp] lemma coe_bracket_of_module (x : L') (m : M) : ⁅x, m⁆ = ⁅(x : L), m⁆ := rfl
+
+/-- 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 :=
+{ 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], }
+
+end lie_module
+
 end lie_subalgebra
 
 variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂]