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 endomorphismsLinearMap.hasEigenvalue_zero_tfae
: equivalent characterizations of endomorphisms with eigenvalue 0LinearMap.not_hasEigenvalue_zero_tfae
: endomorphisms without eigenvalue 0LinearMap.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.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)
:
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)
:
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