English
For a bilinear form Φ on a Lie algebra L, lieInvariant holds iff Φ lies in the maximal triv submodule of BilinForm under the L-action.
Русский
Для билинейной формы Φ на Ли-алгебре L условие инвариантности относительно действия L эквивалентно тому, что Φ лежит в максимальном тривиальном подмодуле BilinForm по действию L.
LaTeX
$$$$ \text{lieInvariant}(L,Φ) \iff Φ \in \operatorname{maxTrivSubmodule}_{L}(\text{BilinForm}). $$$$
Lean4
theorem atomistic : ∀ I : LieIdeal K L, sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I :=
by
intro I
apply le_antisymm
· apply sSup_le
rintro J ⟨-, hJ'⟩
exact hJ'
by_cases hI : I = ⊥
· exact hI.le.trans bot_le
obtain ⟨J, hJ, hJI⟩ := (eq_bot_or_exists_atom_le I).resolve_left hI
let J' := orthogonal Φ hΦ_inv J
suffices I ≤ J ⊔ (J' ⊓ I) by
refine this.trans ?_
apply sup_le
· exact le_sSup ⟨hJ, hJI⟩
rw [← atomistic (J' ⊓ I)]
apply sSup_le_sSup
simp only [le_inf_iff, Set.setOf_subset_setOf, and_imp]
tauto
suffices J ⊔ J' = ⊤ by rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]
exact (orthogonal_isCompl Φ hΦ_nondeg hΦ_inv hΦ_refl hL J hJ).codisjoint.eq_top
termination_by I => finrank K I
decreasing_by
apply finrank_lt_finrank_of_lt
suffices ¬I ≤ J' by simpa
intro hIJ'
apply hJ.1
rw [eq_bot_iff]
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL J hJ le_rfl (hJI.trans hIJ')
