English
The family of generalized eigenspaces { genEigenspace(f, μ) k : μ ∈ R } is independent in the sense of iSupIndep.
Русский
Семейство обобщённых эйгенпространств { genEigenspace(f, μ) k : μ ∈ R } является независимым в смысле iSupIndep.
LaTeX
$$$\\mathrm{iSupIndep}\\bigl(\\,f.genEigenspace(\\cdot) k\\bigr).$$$
Lean4
theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) : iSupIndep (f.genEigenspace · k) :=
by
classical
suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k) (s.sup fun μ ↦ f.genEigenspace μ k)
by
simp_rw [iSupIndep_iff_supIndep_of_injOn (injOn_genEigenspace f k), Finset.supIndep_iff_disjoint_erase]
exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)
intro μ₁ s
induction s using Finset.induction_on with
| empty => simp
| insert μ₂ s _ ih =>
intro hμ₁₂
obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
specialize ih hμ₁
rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
rintro x ⟨hx, hx'⟩
simp only [SetLike.mem_coe] at hx hx'
suffices x ∈ genEigenspace f μ₂ k
by
rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
exact ⟨hx, this⟩
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
let g := f - μ₂ • 1
simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
peel hy with l hlk hl
simp only [LinearMap.mem_ker] at hl
have hyz : (g ^ l) (y + z) ∈ (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k :=
by
refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
· exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
· rw [SetLike.mem_coe, map_add, hl, zero_add]
suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤ s.sup fun μ ↦ f.genEigenspace μ k by
exact this (Submodule.mem_map_of_mem hz)
simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
refine iSup₂_mono fun μ _ ↦ ?_
rintro - ⟨u, hu, rfl⟩
refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
rwa [ih.eq_bot, Submodule.mem_bot] at hyz
