feat(algebra/lie/basic): define missing inclusion maps (#5207)

src/algebra/lie/basic.lean

@@ -459,9 +459,13 @@ lemma of_associative_ring_bracket (x y : A) : ⁅x, y⁆ = x*y - y*x := rfl
 
 end lie_ring
 
-/-- An Abelian Lie algebra is one in which all brackets vanish. -/
-class is_lie_abelian (L : Type v) [has_bracket L L] [has_zero L] : Prop :=
-(abelian : ∀ (x y : L), ⁅x, y⁆ = 0)
+/-- A Lie (ring) module is trivial iff all brackets vanish. -/
+class lie_module.is_trivial (L : Type v) (M : Type w) [has_bracket L M] [has_zero M] : Prop :=
+(trivial : ∀ (x : L) (m : M), ⁅x, m⁆ = 0)
+
+/-- A Lie algebra is Abelian iff it is trivial as a Lie module over itself. -/
+abbreviation is_lie_abelian (L : Type v) [has_bracket L L] [has_zero L] : Prop :=
+lie_module.is_trivial L L
 
 lemma commutative_ring_iff_abelian_lie_ring : is_commutative A (*) ↔ is_lie_abelian A :=
 begin
@@ -746,6 +750,8 @@ def lie_ideal_subalgebra (I : lie_ideal R L) : lie_subalgebra R L :=
 { lie_mem := by { intros x y hx hy, apply lie_mem_right, exact hy, },
   ..I.to_submodule, }
 
+instance : has_coe (lie_ideal R L) (lie_subalgebra R L) := ⟨λ I, lie_ideal_subalgebra R L I⟩
+
 end lie_ideal
 
 end lie_submodule
@@ -836,6 +842,30 @@ instance : add_comm_monoid (lie_submodule R L M) :=
 
 @[simp] lemma add_eq_sup (N N' : lie_submodule R L M) : N + N' = N ⊔ N' := rfl
 
+section inclusion_maps
+
+/-- The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules. -/
+def incl : N →ₗ⁅R,L⁆ M :=
+{ map_lie := λ x m, rfl,
+  ..submodule.subtype (N : submodule R M) }
+
+@[simp] lemma incl_apply (m : N) : N.incl m = m := rfl
+
+lemma incl_eq_val : (N.incl : N → M) = subtype.val := rfl
+
+variables {N} {N' : lie_submodule R L M} (h : N ≤ N')
+
+/-- Given two nested Lie submodules `N ⊆ N'`, the inclusion `N ↪ N'` is a morphism of Lie modules.-/
+def hom_of_le : N →ₗ⁅R,L⁆ N' :=
+{ map_lie := λ x m, rfl,
+  ..submodule.of_le h }
+
+@[simp] lemma coe_hom_of_le (m : N) : (hom_of_le h m : M) = m := rfl
+
+lemma hom_of_le_apply (m : N) : hom_of_le h m = ⟨m.1, h m.2⟩ := rfl
+
+end inclusion_maps
+
 section lie_span
 
 variables (R L) (s : set M)
@@ -1013,6 +1043,12 @@ by { erw lie_submodule.lie_span_le, exact set.image_subset_iff, }
 lemma gc_map_comap (f : L →ₗ⁅R⁆ L') : galois_connection (map f) (comap f) :=
 λ I I', map_le_iff_le_comap
 
+/-- Regarding an ideal `I` as a subalgebra, the inclusion map into its ambient space is a morphism
+of Lie algebras. -/
+def incl (I : lie_ideal R L) : I →ₗ⁅R⁆ L := (I : lie_subalgebra R L).incl
+
+@[simp] lemma incl_apply (I : lie_ideal R L) (x : I) : I.incl x = x := rfl
+
 end lie_ideal
 
 end lie_submodule_map_and_comap

src/algebra/lie/classical.lean

@@ -121,7 +121,7 @@ begin
   let A := Eb R i j hij,
   let B := Eb R j i hij.symm,
   intros c,
-  have c' : A.val ⬝ B.val = B.val ⬝ A.val := by { rw [←sub_eq_zero, ←sl_bracket, c.abelian], refl, },
+  have c' : A.val ⬝ B.val = B.val ⬝ A.val := by { rw [←sub_eq_zero, ←sl_bracket, c.trivial], refl, },
   have : (1 : R) = 0 := by simpa [matrix.mul_apply, hij] using (congr_fun (congr_fun c' i) i),
   exact one_ne_zero this,
 end