English
If I is an atom in a semisimple setting, then I is a simple Lie algebra.
Русский
Если I — атом в полуприложенном окружении, то I — простая Ли-алгебра.
LaTeX
$$$IsAtom I \Rightarrow IsSimple R I$$$
Lean4
theorem isSimple_of_isAtom (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I
where
non_abelian := IsSemisimple.non_abelian_of_isAtom I hI
eq_bot_or_eq_top := by
-- Suppose that `J` is an ideal of `I`.
intro J
let J' : LieIdeal R L :=
{ __ := J.toSubmodule.map I.incl.toLinearMap
lie_mem :=
by
rintro x _
⟨y, hy, rfl⟩
-- We need to show that `⁅x, y⁆ ∈ J` for any `x ∈ L` and `y ∈ J`.
-- Since `L` is semisimple, `x` is contained
-- in the supremum of `I` and the atoms not equal to `I`.
have hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ { I }) :=
by
nth_rewrite 1 [← sSup_singleton (a := I)]
rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left, IsSemisimple.sSup_atoms_eq_top]
· apply LieSubmodule.mem_top
·
simp only [Set.singleton_subset_iff, Set.mem_setOf_eq, hI]
-- Hence we can write `x` as `a + b` with `a ∈ I`
-- and `b` in the supremum of the atoms not equal to `I`.
rw [LieSubmodule.mem_sup] at hx
obtain ⟨a, ha, b, hb, rfl⟩ := hx
simp only [Submodule.carrier_eq_coe, add_lie, SetLike.mem_coe]
apply add_mem
· simp only [Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists]
erw [Submodule.coe_subtype]
simp only [exists_and_right, exists_eq_right, ha, lie_mem_left, exists_true_left]
exact lie_mem_right R I J ⟨a, ha⟩ y hy
· suffices ⁅b, y.val⁆ = 0 by erw [this]; simp only [zero_mem]
rw [← LieSubmodule.mem_bot (R := R) (L := L), ← (IsSemisimple.sSupIndep_isAtom hI).eq_bot]
exact ⟨lie_mem_right R L I b y y.2, lie_mem_left _ _ _ _ _ hb⟩ }
-- Now that we know that `J` is an ideal of `L`,
-- we start with the proof that `I` is a simple Lie algebra.
-- Assume that `J ≠ ⊤`.
rw [or_iff_not_imp_right]
intro hJ
suffices J' = ⊥ by
rw [eq_bot_iff] at this ⊢
intro x hx
suffices x ∈ J → x = 0 from this hx
have := @this x.1
simp only [LieIdeal.incl_coe, LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.mem_mk_iff', Submodule.mem_map,
LieSubmodule.mem_toSubmodule, Subtype.exists, LieSubmodule.mem_bot, ZeroMemClass.coe_eq_zero,
forall_exists_index, and_imp, J'] at this
exact fun _ ↦ this (↑x) x.property hx rfl
apply hI.2
rw [lt_iff_le_and_ne]
constructor
-- We know that `J ≤ I` since `J` is an ideal of `I`.
· rintro _ ⟨x, -, rfl⟩
exact
x.2
-- So we need to show `J ≠ I` as ideals of `L`.
-- This follows from our assumption that `J ≠ ⊤` as ideals of `I`.
contrapose! hJ
rw [eq_top_iff]
rintro ⟨x, hx⟩ -
rw [← hJ] at hx
rcases hx with ⟨y, hy, rfl⟩
exact hy
