Results on the eigenvalue 0

In this file we provide equivalent characterizations of properties related to the eigenvalue 0, such as being nilpotent, having determinant equal to 0, having a non-trivial kernel, etc...

Main results

• LinearMap.charpoly_nilpotent_tfae: equivalent characterizations of nilpotent endomorphisms
• LinearMap.hasEigenvalue_zero_tfae: equivalent characterizations of endomorphisms with eigenvalue 0
• LinearMap.not_hasEigenvalue_zero_tfae: endomorphisms without eigenvalue 0
• LinearMap.finrank_maxGenEigenspace: the dimension of the maximal generalized eigenspace of an endomorphism is the trailing degree of its characteristic polynomial

theorem IsNilpotent.charpoly_eq_X_pow_finrank {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] {φ : Module.End R M} (h : IsNilpotent φ) : LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M

theorem LinearMap.isNilpotent_iff_charpoly {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] (φ : Module.End R M) : IsNilpotent φ ↔ LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M

theorem LinearMap.charpoly_nilpotent_tfae {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] [IsNoetherian R M] (φ : Module.End R M) : [IsNilpotent φ, LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M, ∀ (m : M), ∃ (n : ℕ), (φ ^ n) m = 0, (LinearMap.charpoly φ).natTrailingDegree = Module.finrank R M].TFAE

theorem LinearMap.charpoly_eq_X_pow_iff {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] [IsNoetherian R M] (φ : Module.End R M) : LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M ↔ ∀ (m : M), ∃ (n : ℕ), (φ ^ n) m = 0

theorem LinearMap.hasEigenvalue_zero_tfae {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < LinearMap.ker φ, ∃ (m : M), m ≠ 0 ∧ φ m = 0].TFAE

theorem LinearMap.charpoly_constantCoeff_eq_zero_iff {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : Polynomial.constantCoeff (LinearMap.charpoly φ) = 0 ↔ ∃ (m : M), m ≠ 0 ∧ φ m = 0

theorem LinearMap.not_hasEigenvalue_zero_tfae {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, LinearMap.ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE

theorem LinearMap.finrank_maxGenEigenspace {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : Module.finrank K ↥(φ.maxGenEigenspace 0) = (LinearMap.charpoly φ).natTrailingDegree