restrict_orthogonal_nondegenerate

English

Under assumptions, the atomistic characterization yields a refined decomposition of ideals by atoms.

Русский

При определённых предположениях атомистическое разложение идеалов даёт более тонкую декомпозицию идеалов по атомам.

LaTeX

$$$$ \text{Atomistic decomposition of ideals: } I = \sup\{ J : J \text{ atom} \land J \le I\}. $$$$

Lean4

theorem restrict_orthogonal_nondegenerate (I : LieIdeal K L) (hI : IsAtom I) :
    (Φ.restrict (orthogonal Φ hΦ_inv I)).Nondegenerate :=
  by
  rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]
  simp only [LieIdeal.toLieSubalgebra_toSubmodule, orthogonal_toSubmodule,
    LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]
  exact (orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm

Похожие утверждения