English
Under suitable assumptions (finite-dim), the supremum over χ of the infimum over i of maxGenEigenspace(χ_i) equals the top subspace.
Русский
При разумных предположениях суммарная верхняя граница по χ даёт верхнее подпространство.
LaTeX
$$$$ \bigvee_{\chi} \bigwedge_{i} (f_i).maxGenEigenspace(\chi(i)) = \top. $$$$
Lean4
theorem eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : K[X]) (hq : degree q = 1) :
eigenspace f (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (aeval f q) :=
calc
eigenspace f (-q.coeff 0 / q.leadingCoeff)
_ = LinearMap.ker (q.leadingCoeff • f - algebraMap K (End K V) (-q.coeff 0)) :=
by
rw [eigenspace_div]
intro h
rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq
cases hq
_ = LinearMap.ker (aeval f (C q.leadingCoeff * X + C (q.coeff 0))) := by rw [C_mul', aeval_def];
simp [algebraMap, Algebra.algebraMap]
_ = LinearMap.ker (aeval f q) := by rwa [← eq_X_add_C_of_degree_eq_one]
