Documentation

Mathlib.LinearAlgebra.Eigenspace.Zero

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 #

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.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 = 0m = 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