English
A commuting family of symmetric linear maps on a finite-dimensional inner product space can be diagonalized in a common basis.
Русский
Коммутирующаяся семейство симметричных линейных отображений в общем базисе диагонализуется.
LaTeX
$$$\bigvee_{\chi} \bigwedge_{i} \operatorname{Eig}(T_i, \chi(i)) = \top$$$
Lean4
/-- A commuting family of symmetric linear maps on a finite-dimensional inner
product space is simultaneously diagonalizable. -/
theorem iSup_iInf_eq_top_of_commute {ι : Type*} {T : ι → E →ₗ[𝕜] E} (hT : ∀ i, (T i).IsSymmetric)
(h : Pairwise (Commute on T)) : ⨆ χ : ι → 𝕜, ⨅ i, eigenspace (T i) (χ i) = ⊤ :=
calc
_ = ⨆ χ : ι → 𝕜, ⨅ i, maxGenEigenspace (T i) (χ i) :=
congr(⨆ χ : ι → 𝕜, ⨅ i, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) (χ _))).symm
_ = ⊤ :=
iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute T h fun _ ↦ by
rw [← orthogonal_eq_bot_iff, congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
(hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]
