English
Generalized eigenrange and generalized eigenspace for exponent finrank K V are disjoint.
Русский
Обобщённый диапазон собственных значений и обобщённое собственное подпространство с показателем finrank(K,V) не пересекаются кроме нуля.
LaTeX
$$$\\mathrm{Disjoint}\\big( f.\\mathrm{genEigenrange}(\\mu, \\mathrm{finrank}\\,K V), f.\\mathrm{genEigenspace}(\\mu, \\mathrm{finrank}\\,K V) \\big)$$$
Lean4
/-- Generalized eigenrange and generalized eigenspace for exponent `finrank K V` are disjoint. -/
theorem generalized_eigenvec_disjoint_range_ker [FiniteDimensional K V] (f : End K V) (μ : K) :
Disjoint (f.genEigenrange μ (finrank K V)) (f.genEigenspace μ (finrank K V)) :=
by
have h :=
calc
Submodule.comap ((f - μ • 1) ^ finrank K V) (f.genEigenspace μ (finrank K V)) =
LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V * (f - algebraMap K (End K V) μ) ^ finrank K V) :=
by rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
_ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by simp_rw [← pow_add, genEigenspace_nat]; rfl
_ = f.genEigenspace μ (finrank K V) := by rw [genEigenspace_eq_genEigenspace_finrank_of_le]; cutsat
rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map, Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h,
genEigenspace_nat]
apply Submodule.map_comap_le
