feat: a family of generalized eigenvalues for a commuting linear fami…

…ly of endomorphims must be linear (#8656)

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -495,6 +495,63 @@ theorem map_generalizedEigenrange_le {f : End K V} {μ : K} {n : ℕ} :
 
 #align module.End.map_generalized_eigenrange_le Module.End.map_generalizedEigenrange_le
 
+lemma iSup_generalizedEigenspace_le_smul (f : Module.End R M) (μ t : R) :
+    (⨆ k, f.generalizedEigenspace μ k) ≤ ⨆ k, (t • f).generalizedEigenspace (t * μ) k := by
+  intro m hm
+  simp only [Submodule.mem_iSup_of_chain, mem_generalizedEigenspace] at hm ⊢
+  refine Exists.imp (fun k hk ↦ ?_) hm
+  rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hk, smul_zero]
+
+lemma iSup_generalizedEigenspace_inf_le_add
+    (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) :
+    (⨆ k, f₁.generalizedEigenspace μ₁ k) ⊓ (⨆ k, f₂.generalizedEigenspace μ₂ k) ≤
+    ⨆ k, (f₁ + f₂).generalizedEigenspace (μ₁ + μ₂) k := by
+  intro m hm
+  simp only [iSup_le_iff, Submodule.mem_inf, Submodule.mem_iSup_of_chain,
+    mem_generalizedEigenspace] at hm ⊢
+  obtain ⟨⟨k₁, hk₁⟩, ⟨k₂, hk₂⟩⟩ := hm
+  use k₁ + k₂ - 1
+  have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by
+    rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
+  replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) :=
+    (h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left
+      (Algebra.commute_algebraMap_left μ₁ _)
+  rw [this, h.add_pow', LinearMap.coeFn_sum, Finset.sum_apply]
+  refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_
+  suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
+    rw [LinearMap.smul_apply, this, smul_zero]
+  cases' Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi hj
+  · rw [(h.pow_pow i j).eq, LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hi hk₁,
+      LinearMap.map_zero]
+  · rw [LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hj hk₂, LinearMap.map_zero]
+
+lemma map_smul_of_iInf_generalizedEigenspace_ne_bot [NoZeroSMulDivisors R M]
+    {L F : Type*} [SMul R L] [SMulHomClass F R L (End R M)] (f : F)
+    (μ : L → R) (h_ne : ⨅ x, ⨆ k, (f x).generalizedEigenspace (μ x) k ≠ ⊥)
+    (t : R) (x : L) :
+    μ (t • x) = t • μ x := by
+  by_contra contra
+  let g : L → Submodule R M := fun x ↦ ⨆ k, (f x).generalizedEigenspace (μ x) k
+  have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
+  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
+  apply Disjoint.mono_left (iSup_generalizedEigenspace_le_smul (f x) (μ x) t)
+  simp only [map_smul]
+  exact disjoint_iSup_generalizedEigenspace (t • f x) (Ne.symm contra)
+
+lemma map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M]
+    {L F : Type*} [Add L] [AddHomClass F L (End R M)] (f : F)
+    (μ : L → R) (h_ne : ⨅ x, ⨆ k, (f x).generalizedEigenspace (μ x) k ≠ ⊥)
+    (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
+    μ (x + y) = μ x + μ y := by
+  by_contra contra
+  let g : L → Submodule R M := fun x ↦ ⨆ k, (f x).generalizedEigenspace (μ x) k
+  have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
+    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
+  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
+  apply Disjoint.mono_left (iSup_generalizedEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) (h x y))
+  simp only [map_add]
+  exact disjoint_iSup_generalizedEigenspace (f x + f y) (Ne.symm contra)
+
 end End
 
 end Module