English
Under hypotheses including a nondegenerate invariant form Φ and a reflexive condition, the Lie submodule generated by the orthogonal of a Lie ideal I is the complement to I in a semisimple setting; equivalently, I and its orthogonal form a complementary pair.
Русский
При условии, что Φ невырожденна и инвариантна, а также при некоторых рефлексивных условиях, подмодуль порождается ортотангенсом идеала I и образует комплементарную пару.
LaTeX
$$$$ \text{IsCompl}(I, \operatorname{orthogonal}_{Φ}(I)). $$$$
Lean4
theorem orthogonal_isCompl_toSubmodule (I : LieIdeal K L) (hI : IsAtom I) :
IsCompl I.toSubmodule (orthogonal Φ hΦ_inv I).toSubmodule :=
by
rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl, ←
orthogonal_toSubmodule _ hΦ_inv, LieSubmodule.disjoint_toSubmodule]
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI
