feat(algebra/lie/semisimple): adjoint action is injective for semisim…

…ple Lie algebras (#8698)
leanprover-community · Aug 16, 2021 · deedf25 · deedf25
1 parent c416a48
commit deedf25
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/algebra/lie/abelian.lean b/src/algebra/lie/abelian.lean
@@ -213,7 +213,9 @@ abbreviation center : lie_ideal R L := lie_module.max_triv_submodule R L L
 
 instance : is_lie_abelian (center R L) := infer_instance
 
-lemma center_eq_adjoint_kernel : center R L = lie_module.ker R L L :=
+@[simp] lemma ad_ker_eq_self_module_ker : (ad R L).ker = lie_module.ker R L L := rfl
+
+@[simp] lemma self_module_ker_eq_center : lie_module.ker R L L = center R L :=
 begin
   ext y,
   simp only [lie_module.mem_max_triv_submodule, lie_module.mem_ker, ← lie_skew _ y, neg_eq_zero],

diff --git a/src/algebra/lie/semisimple.lean b/src/algebra/lie/semisimple.lean
@@ -110,4 +110,7 @@ begin
   { intros h, apply h, apply_instance, },
 end
 
+lemma ad_ker_eq_bot_of_semisimple [is_semisimple R L] : (ad R L).ker = ⊥ :=
+by simp
+
 end lie_algebra