diff --git a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean index 868496a0b3462..2d9e68f494ca4 100644 --- a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean +++ b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean @@ -9,10 +9,10 @@ import Mathlib.Analysis.InnerProductSpace.Projection import Mathlib.Order.CompleteLattice import Mathlib.LinearAlgebra.Eigenspace.Basic -/-! # Joint eigenspaces of a commuting pair of symmetric operators +/-! # Joint eigenspaces of commuting symmetric operators -This file collects various decomposition results for joint eigenspaces of a commuting pair -of symmetric operators on a finite-dimensional inner product space. +This file collects various decomposition results for joint eigenspaces of commuting +symmetric operators on a finite-dimensional inner product space. # Main Result @@ -20,6 +20,9 @@ of symmetric operators on a finite-dimensional inner product space. if `{A B : E →ₗ[𝕜] E}`, then `IsSymmetric A`, `IsSymmetric B` and `A ∘ₗ B = B ∘ₗ A` imply that `E` decomposes as an internal direct sum of the pairwise orthogonal spaces `eigenspace B μ ⊓ eigenspace A ν` +* `LinearMap.IsSymmetric.directSum_isInternal_of_commute_of_fintype` establishes the + analogous result to `LinearMap.IsSymmetric.directSum_isInternal_of_commute` for finite commuting + tuples of symmetric operators. ## TODO @@ -28,32 +31,27 @@ and a proof obligation that the basis vectors are eigenvectors. ## Tags -self-adjoint operator, simultaneous eigenspaces, joint eigenspaces +symmetric operator, simultaneous eigenspaces, joint eigenspaces -/ -variable {𝕜 E : Type*} [RCLike 𝕜] -variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - open Module.End namespace LinearMap namespace IsSymmetric -section Pair +variable {𝕜 E n m : Type*} + +open Submodule -variable {α : 𝕜} {A B : E →ₗ[𝕜] E} +section RCLike -/--If a pair of operators commute, then the eigenspaces of one are invariant under the other.-/ -theorem eigenspace_invariant_of_commute - (hAB : A ∘ₗ B = B ∘ₗ A) (α : 𝕜) : ∀ v ∈ (eigenspace A α), (B v ∈ eigenspace A α) := by - intro v hv - rw [eigenspace, mem_ker, sub_apply, Module.algebraMap_end_apply, ← comp_apply A B v, hAB, - comp_apply B A v, ← map_smul, ← map_sub, hv, map_zero] at * +variable [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] +variable {α : 𝕜} {A B : E →ₗ[𝕜] E} {T : n → E →ₗ[𝕜] E} -/--The simultaneous eigenspaces of a pair of commuting symmetric operators form an -`OrthogonalFamily`.-/ +/-- The joint eigenspaces of a pair of commuting symmetric operators form an +`OrthogonalFamily`. -/ theorem orthogonalFamily_eigenspace_inf_eigenspace (hA : A.IsSymmetric) (hB : B.IsSymmetric) : OrthogonalFamily 𝕜 (fun (i : 𝕜 × 𝕜) => (eigenspace A i.2 ⊓ eigenspace B i.1 : Submodule 𝕜 E)) (fun i => (eigenspace A i.2 ⊓ eigenspace B i.1).subtypeₗᵢ) := @@ -63,35 +61,38 @@ theorem orthogonalFamily_eigenspace_inf_eigenspace (hA : A.IsSymmetric) (hB : B. · exact hB.orthogonalFamily_eigenspaces.pairwise h₁ hv2 w hw2 · exact hA.orthogonalFamily_eigenspaces.pairwise h₂ hv1 w hw1 -open Submodule in - -/-- The intersection of eigenspaces of commuting selfadjoint operators is equal to the eigenspace of -one operator restricted to the eigenspace of the other, which is an invariant subspace because the -operators commute. -/ -theorem eigenspace_inf_eigenspace - (hAB : A ∘ₗ B = B ∘ₗ A) (γ : 𝕜) : - eigenspace A α ⊓ eigenspace B γ = map (Submodule.subtype (eigenspace A α)) - (eigenspace (B.restrict (eigenspace_invariant_of_commute hAB α)) γ) := - (eigenspace A α).inf_genEigenspace _ _ (k := 1) +/-- The joint eigenspaces of a tuple of commuting symmetric operators form an +`OrthogonalFamily`. -/ +theorem orthogonalFamily_iInf_eigenspaces + (hT : ∀ i, (T i).IsSymmetric) : + OrthogonalFamily 𝕜 (fun γ : n → 𝕜 ↦ (⨅ j, eigenspace (T j) (γ j) : Submodule 𝕜 E)) + fun γ : n → 𝕜 ↦ (⨅ j, eigenspace (T j) (γ j)).subtypeₗᵢ := by + intro f g hfg Ef Eg + obtain ⟨a , ha⟩ := Function.ne_iff.mp hfg + have H := (orthogonalFamily_eigenspaces (hT a) ha) + simp only [Submodule.coe_subtypeₗᵢ, Submodule.coeSubtype, Subtype.forall] at H + apply H + · exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _ + · exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _ variable [FiniteDimensional 𝕜 E] /-- If A and B are commuting symmetric operators on a finite dimensional inner product space -then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace.-/ -theorem iSup_eigenspace_inf_eigenspace (hB : B.IsSymmetric) - (hAB : A ∘ₗ B = B ∘ₗ A): +then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace. -/ +theorem iSup_eigenspace_inf_eigenspace (hB : B.IsSymmetric) (hAB : Commute A B) : (⨆ γ, eigenspace A α ⊓ eigenspace B γ) = eigenspace A α := by conv_rhs => rw [← (eigenspace A α).map_subtype_top] - simp only [eigenspace_inf_eigenspace hAB, ← Submodule.map_iSup] + simp only [← Module.End.genEigenspace_one B, ← Submodule.map_iSup, + (eigenspace A α).inf_genEigenspace _ (mapsTo_genEigenspace_of_comm hAB α 1)] congr 1 - rw [← Submodule.orthogonal_eq_bot_iff] - exact orthogonalComplement_iSup_eigenspaces_eq_bot <| - hB.restrict_invariant <| eigenspace_invariant_of_commute hAB α + simpa only [Module.End.genEigenspace_one, Submodule.orthogonal_eq_bot_iff] + using orthogonalComplement_iSup_eigenspaces_eq_bot <| + hB.restrict_invariant <| mapsTo_genEigenspace_of_comm hAB α 1 /-- If A and B are commuting symmetric operators acting on a finite dimensional inner product space, then the simultaneous eigenspaces of A and B exhaust the space. -/ theorem iSup_iSup_eigenspace_inf_eigenspace_eq_top (hA : A.IsSymmetric) (hB : B.IsSymmetric) - (hAB : A ∘ₗ B = B ∘ₗ A) : + (hAB : Commute A B) : (⨆ α, ⨆ γ, eigenspace A α ⊓ eigenspace B γ) = ⊤ := by simpa [iSup_eigenspace_inf_eigenspace hB hAB] using Submodule.orthogonal_eq_bot_iff.mp <| hA.orthogonalComplement_iSup_eigenspaces_eq_bot @@ -99,14 +100,67 @@ theorem iSup_iSup_eigenspace_inf_eigenspace_eq_top (hA : A.IsSymmetric) (hB : B. /-- Given a commuting pair of symmetric linear operators on a finite dimensional inner product space, the space decomposes as an internal direct sum of simultaneous eigenspaces of these operators. -/ -theorem directSum_isInteral_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric) - (hAB : A ∘ₗ B = B ∘ₗ A) : +theorem directSum_isInternal_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric) + (hAB : Commute A B) : DirectSum.IsInternal (fun (i : 𝕜 × 𝕜) ↦ (eigenspace A i.2 ⊓ eigenspace B i.1)):= by apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm] exact iSup_iSup_eigenspace_inf_eigenspace_eq_top hA hB hAB -end Pair +/-- If `F` is an invariant subspace of a symmetric operator `S`, then `F` is the supremum of the +eigenspaces of the restriction of `S` to `F`. -/ +theorem iSup_eigenspace_restrict {F : Submodule 𝕜 E} + (S : E →ₗ[𝕜] E) (hS : IsSymmetric S) (hInv : Set.MapsTo S F F) : + ⨆ μ, map F.subtype (eigenspace (S.restrict hInv) μ) = F := by + conv_lhs => rw [← Submodule.map_iSup] + conv_rhs => rw [← map_subtype_top F] + congr! + have H : IsSymmetric (S.restrict hInv) := fun x y ↦ hS (F.subtype x) y + apply orthogonal_eq_bot_iff.mp (H.orthogonalComplement_iSup_eigenspaces_eq_bot) + +/-- The orthocomplement of the indexed supremum of joint eigenspaces of a finite commuting tuple of +symmetric operators is trivial. -/ +theorem orthogonalComplement_iSup_iInf_eigenspaces_eq_bot [Finite n] + (hT : ∀ i, (T i).IsSymmetric) (hC : ∀ i j, Commute (T i) (T j)) : + (⨆ γ : n → 𝕜, ⨅ j, eigenspace (T j) (γ j))ᗮ = ⊥ := by + have _ := Fintype.ofFinite n + revert T + change ∀ T, _ + refine Fintype.induction_subsingleton_or_nontrivial n (fun m _ hhm T hT _ ↦ ?_) + (fun m hm hmm H T hT hC ↦ ?_) + · obtain (hm | hm) := isEmpty_or_nonempty m + · simp + · have := uniqueOfSubsingleton (Classical.choice hm) + simpa only [ciInf_unique, ← (Equiv.funUnique m 𝕜).symm.iSup_comp] + using hT default |>.orthogonalComplement_iSup_eigenspaces_eq_bot + · have i := Classical.arbitrary m + classical + specialize H {x // x ≠ i} (Fintype.card_subtype_lt (x := i) (by simp)) + (Subtype.restrict (· ≠ i) T) (hT ·) (hC · ·) + simp only [Submodule.orthogonal_eq_bot_iff] at * + rw [← (Equiv.funSplitAt i 𝕜).symm.iSup_comp, iSup_prod, iSup_comm] + convert H with γ + rw [← iSup_eigenspace_restrict (T i) (hT i) (F := ⨅ j, eigenspace _ _)] + swap + · exact mapsTo_iInf_genEigenspace_of_forall_comm (fun j : {j // j ≠ i} ↦ hC j i) γ 1 + congr! with μ + rw [← Module.End.genEigenspace_one, ← Submodule.inf_genEigenspace _ _ _ (k := 1), inf_comm, + iInf_split_single _ i, iInf_subtype] + congr! with x hx + · simp + · simp [dif_neg hx] + +/-- Given a finite commuting family of symmetric linear operators, the Hilbert space on which they +act decomposes as an internal direct sum of simultaneous eigenspaces. -/ +theorem LinearMap.IsSymmetric.directSum_isInternal_of_commute_of_fintype [Finite n] + [DecidableEq (n → 𝕜)] (hT :∀ i, (T i).IsSymmetric) + (hC : ∀ i j, Commute (T i) (T j)) : + DirectSum.IsInternal (fun α : n → 𝕜 ↦ ⨅ j, eigenspace (T j) (α j)) := by + rw [OrthogonalFamily.isInternal_iff] + · exact orthogonalComplement_iSup_iInf_eigenspaces_eq_bot hT hC + · exact orthogonalFamily_iInf_eigenspaces hT + +end RCLike end IsSymmetric diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index e5c7fcb4b592f..3cc53b426884f 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -181,6 +181,11 @@ theorem genEigenspace_zero (f : End R M) (k : ℕ) : f.genEigenspace 0 k = LinearMap.ker (f ^ k) := by simp [Module.End.genEigenspace] +@[simp] +theorem genEigenspace_one (f : End R M) (μ : R) : + f.genEigenspace μ 1 = f.eigenspace μ := + rfl + /-- A nonzero element of a generalized eigenspace is a generalized eigenvector. (Def 8.9 of [axler2015])-/ def HasGenEigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop := @@ -306,6 +311,15 @@ lemma mapsTo_iSup_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : rintro x ⟨k, hk⟩ exact ⟨k, f.mapsTo_genEigenspace_of_comm h μ k hk⟩ +lemma mapsTo_iInf_genEigenspace_of_forall_comm {ι R M : Type*} [CommRing R] [AddCommGroup M] + [Module R M] {f : ι → Module.End R M} {g : Module.End R M} (hC : ∀ j, Commute (f j) g) + (μ : ι → R) (k : ℕ) : + MapsTo g + (⨅ j, genEigenspace (f j) (μ j) k : Submodule R M) + (⨅ j, genEigenspace (f j) (μ j) k : Submodule R M) := by + rw [Submodule.iInf_coe] + exact mapsTo_iInter_iInter fun j ↦ mapsTo_genEigenspace_of_comm (hC j) (μ j) k + /-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent. -/ lemma isNilpotent_restrict_sub_algebraMap (f : End R M) (μ : R) (k : ℕ) (h : MapsTo (f - algebraMap R (End R M) μ)