English
Assuming p is closed under f and h, the p-generated iSup of genEigenspace μ k equals the iSup of p ⊓ f.genEigenspace μ k.
Русский
Пусть p замкнут относительно f; тогда равенство между iSup и инфимумами держится: p = ⊔μ (p ∩ f.genEigenspace μ k).
LaTeX
$$$p = \\bigvee_{\\mu} (p \\cap f.genEigenspace(\\mu, k)).$$$
Lean4
theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (k : ℕ∞) :
p ⊓ ⨆ μ, f.genEigenspace μ k = ⨆ μ, p ⊓ f.genEigenspace μ k :=
by
refine le_antisymm (fun m hm ↦ ?_) (le_inf_iff.mpr ⟨iSup_le fun μ ↦ inf_le_left, iSup_mono fun μ ↦ inf_le_right⟩)
classical
obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, f.genEigenspace μ k⟩ := hm
obtain ⟨m, hm₂, rfl⟩ := (mem_iSup_iff_exists_finsupp _ _).mp hm₁
suffices ∀ μ, (m μ : V) ∈ p by
exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩
intro μ
by_cases hμ : μ ∈ m.support; swap
· simp only [Finsupp.notMem_support_iff.mp hμ, p.zero_mem]
have hm₂_aux := hm₂
simp_rw [Module.End.mem_genEigenspace] at hm₂_aux
choose l hlk hl using hm₂_aux
let l₀ : ℕ := m.support.sup l
have h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - algebraMap K (End K V) μ₁) ^ l₀) ((f - algebraMap K (End K V) μ₂) ^ l₀) :=
fun μ₁ μ₂ ↦
((Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).sub_left
(Algebra.commute_algebraMap_left _ _)).pow_pow
_ _
let g : End K V := (m.support.erase μ).noncommProd _ fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂
have hfg : Commute f g :=
Finset.noncommProd_commute _ _ _ _ fun μ' _ ↦
(Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).pow_right _
have hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ) :=
by
suffices ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0 by
rw [map_finsuppSum, Finsupp.sum_congr (g2 := fun μ' _ ↦ if μ' = μ then g (m μ) else 0) this, Finsupp.sum_ite_eq',
if_pos hμ]
rintro μ' hμ'
split_ifs with hμμ'
· rw [hμμ']
have hl₀ : ((f - algebraMap K (End K V) μ') ^ l₀) (m μ') = 0 :=
by
rw [← LinearMap.mem_ker, Algebra.algebraMap_eq_smul_one, ← End.mem_genEigenspace_nat]
simp_rw [← End.mem_genEigenspace_nat] at hl
suffices (l μ' : ℕ∞) ≤ l₀ from (f.genEigenspace μ').mono this (hl μ')
simpa only [Nat.cast_le] using Finset.le_sup hμ'
have : _ = g :=
(m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩)
(fun μ ↦ (f - algebraMap K (End K V) μ) ^ l₀) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂)
rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
have hg₁ : MapsTo g p p :=
Finset.noncommProd_induction _ _ _ (fun g' : End K V ↦ MapsTo g' p p) (fun f₁ f₂ ↦ MapsTo.comp) (mapsTo_id _)
fun μ' _ ↦
by
suffices MapsTo (f - algebraMap K (End K V) μ') p p by simp only [Module.End.coe_pow, this.iterate l₀]
intro x hx
rw [LinearMap.sub_apply, algebraMap_end_apply]
exact p.sub_mem (h _ hx) (smul_mem p μ' hx)
have hg₂ : MapsTo g ↑(f.genEigenspace μ k) ↑(f.genEigenspace μ k) := f.mapsTo_genEigenspace_of_comm hfg μ k
have hg₃ : InjOn g ↑(f.genEigenspace μ k) :=
by
apply LinearMap.injOn_of_disjoint_ker subset_rfl
have this := f.independent_genEigenspace k
have aux (μ') (_hμ' : μ' ∈ m.support.erase μ) : (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k :=
by
apply (f.genEigenspace μ').mono
rintro k rfl
simp only [ENat.some_eq_coe, Nat.cast_inj, exists_eq_left']
apply Finset.sup_le
intro i _hi
simpa using hlk i
rw [LinearMap.ker_noncommProd_eq_of_supIndep_ker, ← Finset.sup_eq_iSup]
· have := Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ
apply this.mono_right
apply Finset.sup_mono_fun
intro μ' hμ'
rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
apply aux μ' hμ'
· have := this.supIndep' (m.support.erase μ)
apply this.antitone_fun
intro μ' hμ'
rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
apply aux μ' hμ'
have hg₄ : SurjOn g ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) :=
by
have : MapsTo g ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) := hg₁.inter_inter hg₂
rw [← LinearMap.injOn_iff_surjOn this]
exact hg₃.mono inter_subset_right
specialize hm₂ μ
obtain ⟨y, ⟨hy₀ : y ∈ p, hy₁ : y ∈ f.genEigenspace μ k⟩, hy₂ : g y = g (m μ)⟩ := hg₄ ⟨(hg₀ ▸ hg₁ hm₀), hg₂ hm₂⟩
rwa [← hg₃ hy₁ hm₂ hy₂]
