directSum_isInternal_of_pairwise_commute

English

For a commuting family of symmetric linear maps, the internal direct sum of the joint eigenspaces (indexed by eigenvalues) gives the whole space.

Русский

Для коммутирующей пары симметричных отображений внутренная прямая сумма совместных собственных пространств охватывает всё пространство.

LaTeX

$$DirectSum.IsInternal (fun i => (eigenspace (T i) (i)))$$

Lean4

/-- In finite dimensions, given a commuting family of symmetric linear operators, the inner
product space on which they act decomposes as an internal direct sum of joint eigenspaces. -/
theorem directSum_isInternal_of_pairwise_commute [DecidableEq (n → 𝕜)] (hT : ∀ i, (T i).IsSymmetric)
    (hC : Pairwise (Commute on T)) : DirectSum.IsInternal (fun α : n → 𝕜 ↦ ⨅ j, eigenspace (T j) (α j)) :=
  by
  rw [OrthogonalFamily.isInternal_iff]
  · rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]
  · exact orthogonalFamily_iInf_eigenspaces hT

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