English
A list of equivalent conditions for having eigenvalue 0: HasEigenvalue 0, IsRoot 0 for minpoly, constantCoeff of charpoly equal 0, det φ = 0, ker φ ≠ ⊥, and the existence of a nonzero vector mapped to 0.
Русский
Эквивалентности наличия корня 0: HasEigenvalue 0, IsRoot 0 для minpoly, константный коэффициент charpoly равен 0, det φ = 0, ker φ ≠ ⊥, и существование ненулевого v с φ(v) = 0.
LaTeX
$$$[Module.End.HasEigenvalue φ 0, (\\minpoly K φ).IsRoot 0, constantCoeff φ.charpoly = 0, LinearMap.det φ = 0, ⊥ < ker φ, ∃ m ≠ 0, φ m = 0]$ является эквивалентной цепочкой.$$
Lean4
theorem hasEigenvalue_zero_tfae (φ : Module.End K M) :
List.TFAE
[Module.End.HasEigenvalue φ 0, IsRoot (minpoly K φ) 0, constantCoeff φ.charpoly = 0, LinearMap.det φ = 0,
⊥ < ker φ, ∃ (m : M), m ≠ 0 ∧ φ m = 0] :=
by
tfae_have 1 ↔ 2 := Module.End.hasEigenvalue_iff_isRoot
tfae_have 2 → 3 := by
obtain ⟨F, hF⟩ := minpoly_dvd_charpoly φ
simp only [IsRoot.def, constantCoeff_apply, coeff_zero_eq_eval_zero, hF, eval_mul]
intro h; rw [h, zero_mul]
tfae_have 3 → 4 :=
by
rw [← LinearMap.det_toMatrix (chooseBasis K M), Matrix.det_eq_sign_charpoly_coeff, constantCoeff_apply, charpoly]
intro h; rw [h, mul_zero]
tfae_have 4 → 5 := bot_lt_ker_of_det_eq_zero
tfae_have 5 → 6 := by
contrapose!
simp only [not_bot_lt_iff, eq_bot_iff]
intro h x
simp only [mem_ker, Submodule.mem_bot]
contrapose!
apply h
tfae_have 6 → 1
| ⟨x, h1, h2⟩ => by
apply Module.End.hasEigenvalue_of_hasEigenvector ⟨_, h1⟩
simpa only [Module.End.eigenspace_zero, mem_ker] using h2
tfae_finish
