English
Explicitly, the atomistic property of the invariant form implies a canonical representation of ideals as suprema of atoms.
Русский
Явление атомистичности формы дает каноническое представление идеалов как наибольших верхних пределов атомов.
LaTeX
$$$$ \text{Atomistic property: } \forall I, \; \sup\{J: J \text{ atom} \land J \le I\} = I. $$$$
Lean4
/-- A finite-dimensional Lie algebra over a field is semisimple
if it does not have non-trivial abelian ideals and it admits a
non-degenerate reflexive invariant bilinear form.
Here a form is *invariant* if it is compatible with the Lie bracket: `Φ ⁅x, y⁆ z = Φ x ⁅y, z⁆`.
-/
theorem isSemisimple_of_nondegenerate : IsSemisimple K L :=
by
refine ⟨?_, ?_, hL⟩
· simpa using atomistic Φ hΦ_nondeg hΦ_inv hΦ_refl hL ⊤
intro I hI
apply (orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI).mono_right
apply sSup_le
simp only [Set.mem_diff, Set.mem_setOf_eq, Set.mem_singleton_iff, and_imp]
intro J hJ hJI
rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]
rintro _ ⟨x, y, rfl⟩
simp only [orthogonal_carrier, Φ.isOrtho_def, Set.mem_setOf_eq]
intro z hz
rw [← neg_eq_zero, ← hΦ_inv]
suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]
rw [← LieSubmodule.mem_bot (R := K) (L := L), ← (hJ.disjoint_of_ne hI hJI).eq_bot]
apply lie_le_inf
exact lie_mem_lie x.2 hz
