Documentation

Mathlib.Algebra.Module.LinearMap.Polynomial

Characteristic polynomials of linear families of endomorphisms #

The coefficients of the characteristic polynomials of a linear family of endomorphisms are homogeneous polynomials in the parameters. This result is used in Lie theory to establish the existence of regular elements and Cartan subalgebras, and ultimately a well-defined notion of rank for Lie algebras.

In this file we prove this result about characteristic polynomials. Let L and M be modules over a nontrivial commutative ring R, and let φ : L →ₗ[R] Module.End R M be a linear map. Let b be a basis of L, indexed by ι. Then we define a multivariate polynomial with variables indexed by ι that evaluates on elements x of L to the characteristic polynomial of φ x.

Main declarations #

Matrix.toMvPolynomial M i: the family of multivariate polynomials that evaluates on c : n → R to the dot product of the i-th row of M with c. Matrix.toMvPolynomial M i is the sum of the monomials C (M i j) * X j.
LinearMap.toMvPolynomial b₁ b₂ f: a version of Matrix.toMvPolynomial for linear maps f with respect to bases b₁ and b₂ of the domain and codomain.
LinearMap.polyCharpoly: the multivariate polynomial that evaluates on elements x of L to the characteristic polynomial of φ x.
LinearMap.polyCharpoly_map_eq_charpoly: the evaluation of polyCharpoly on elements x of L is the characteristic polynomial of φ x.
LinearMap.polyCharpoly_coeff_isHomogeneous: the coefficients of polyCharpoly are homogeneous polynomials in the parameters.
LinearMap.nilRank: the smallest index at which polyCharpoly has a non-zero coefficient, which is independent of the choice of basis for L.
LinearMap.IsNilRegular: an element x of L is nil-regular with respect to φ if the n-th coefficient of the characteristic polynomial of φ x is non-zero, where n denotes the nil-rank of φ.

Implementation details #

We show that LinearMap.polyCharpoly does not depend on the choice of basis of the target module. This is done via LinearMap.polyCharpoly_eq_polyCharpolyAux and LinearMap.polyCharpolyAux_basisIndep. The latter is proven by considering the base change of the R-linear map φ : L →ₗ[R] End R M to the multivariate polynomial ring MvPolynomial ι R, and showing that polyCharpolyAux φ is equal to the characteristic polynomial of this base change. The proof concludes because characteristic polynomials are independent of the chosen basis.

References #

[barnes1967]: "On Cartan subalgebras of Lie algebras" by D.W. Barnes.

noncomputable def Matrix.toMvPolynomial {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) :

MvPolynomial n R

Let M be an (m × n)-matrix over R. Then Matrix.toMvPolynomial M is the family (indexed by i : m) of multivariate polynomials in n variables over R that evaluates on c : n → R to the dot product of the i-th row of M with c: Matrix.toMvPolynomial M i is the sum of the monomials C (M i j) * X j.

Equations

M.toMvPolynomial i = ∑ j : n, (MvPolynomial.monomial (Finsupp.single j 1)) (M i j)

theorem Matrix.toMvPolynomial_eval_eq_apply {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) (c : n → R) :

(MvPolynomial.eval c) (M.toMvPolynomial i) = M.mulVec c i

theorem Matrix.toMvPolynomial_map {m : Type u_1} {n : Type u_2} {R : Type u_4} {S : Type u_5} [Fintype n] [CommSemiring R] [CommSemiring S] (f : R →+* S) (M : Matrix m n R) (i : m) :

(M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)

theorem Matrix.toMvPolynomial_isHomogeneous {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) :

(M.toMvPolynomial i).IsHomogeneous 1

theorem Matrix.toMvPolynomial_totalDegree_le {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) :

(M.toMvPolynomial i).totalDegree ≤ 1

@[simp]

theorem Matrix.toMvPolynomial_constantCoeff {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M : Matrix m n R) (i : m) :

MvPolynomial.constantCoeff (M.toMvPolynomial i) = 0

@[simp]

theorem Matrix.toMvPolynomial_zero {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] :

toMvPolynomial 0 = 0

@[simp]

theorem Matrix.toMvPolynomial_one {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] [DecidableEq n] :

toMvPolynomial 1 = MvPolynomial.X

theorem Matrix.toMvPolynomial_add {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] (M N : Matrix m n R) :

(M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial

theorem Matrix.toMvPolynomial_mul {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [Fintype n] [Fintype o] [CommSemiring R] (M : Matrix m n R) (N : Matrix n o R) (i : m) :

(M * N).toMvPolynomial i = (MvPolynomial.bind₁ N.toMvPolynomial) (M.toMvPolynomial i)

noncomputable def LinearMap.toMvPolynomial {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) :

MvPolynomial ι₁ R

Let f : M₁ →ₗ[R] M₂ be an R-linear map between modules M₁ and M₂ with bases b₁ and b₂ respectively. Then LinearMap.toMvPolynomial b₁ b₂ f is the family of multivariate polynomials over R that evaluates on an element x of M₁ (represented on the basis b₁) to the element f x of M₂ (represented on the basis b₂).

Equations

LinearMap.toMvPolynomial b₁ b₂ f i = ((LinearMap.toMatrix b₁ b₂) f).toMvPolynomial i

theorem LinearMap.toMvPolynomial_eval_eq_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R) :

(MvPolynomial.eval ⇑c) (toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i

theorem LinearMap.toMvPolynomial_baseChange {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type u_6) [CommRing A] [Algebra R A] :

toMvPolynomial (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂) (baseChange A f) i = (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b₁ b₂ f i)

theorem LinearMap.toMvPolynomial_isHomogeneous {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) :

(toMvPolynomial b₁ b₂ f i).IsHomogeneous 1

theorem LinearMap.toMvPolynomial_totalDegree_le {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) :

(toMvPolynomial b₁ b₂ f i).totalDegree ≤ 1

@[simp]

theorem LinearMap.toMvPolynomial_constantCoeff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) :

MvPolynomial.constantCoeff (toMvPolynomial b₁ b₂ f i) = 0

@[simp]

theorem LinearMap.toMvPolynomial_zero {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) :

toMvPolynomial b₁ b₂ 0 = 0

@[simp]

theorem LinearMap.toMvPolynomial_id {R : Type u_1} {M₁ : Type u_2} {ι₁ : Type u_4} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Fintype ι₁] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) :

toMvPolynomial b₁ b₁ id = MvPolynomial.X

theorem LinearMap.toMvPolynomial_add {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Finite ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f g : M₁ →ₗ[R] M₂) :

toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g

theorem LinearMap.toMvPolynomial_comp {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {ι₁ : Type u_5} {ι₂ : Type u_6} {ι₃ : Type u_7} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] [Fintype ι₁] [Fintype ι₂] [Finite ι₃] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (b₃ : Basis ι₃ R M₃) (g : M₂ →ₗ[R] M₃) (f : M₁ →ₗ[R] M₂) (i : ι₃) :

toMvPolynomial b₁ b₃ (g ∘ₗ f) i = (MvPolynomial.bind₁ (toMvPolynomial b₁ b₂ f)) (toMvPolynomial b₂ b₃ g i)

noncomputable def LinearMap.polyCharpolyAux {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) :

Polynomial (MvPolynomial ι R)

(Implementation detail, see LinearMap.polyCharpoly.)

Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear map. Let b be a basis of L and bₘ a basis of M. Then LinearMap.polyCharpolyAux φ b bₘ is the polynomial that evaluates on elements x of L to the characteristic polynomial of φ x acting on M.

This definition does not depend on the choice of bₘ (see LinearMap.polyCharpolyAux_basisIndep).

Equations

φ.polyCharpolyAux b bₘ = Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)

theorem LinearMap.polyCharpolyAux_baseChange {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] :

(tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A bₘ) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)

theorem LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (x : L) :

Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((toMatrix bₘ bₘ) (φ x)).charpoly

theorem LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (x : L) (i : ℕ) :

(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = ((toMatrix bₘ bₘ) (φ x)).charpoly.coeff i

@[simp]

theorem LinearMap.polyCharpolyAux_map_eq_charpoly {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : L) :

Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = charpoly (φ x)

@[simp]

theorem LinearMap.polyCharpolyAux_coeff_eval {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : L) (i : ℕ) :

(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i

theorem LinearMap.polyCharpolyAux_map_eval {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : ι → R) :

Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) = charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))

theorem LinearMap.polyCharpolyAux_map_aeval {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] [Module.Finite A (TensorProduct R A M)] [Module.Free A (TensorProduct R A M)] (x : ι → A) :

Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = ((tensorProduct R A M M ∘ₗ baseChange A φ) ((Algebra.TensorProduct.basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly

theorem LinearMap.polyCharpolyAux_basisIndep {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) {ιM' : Type u_8} [Fintype ιM'] [DecidableEq ιM'] (bₘ' : Basis ιM' R M) :

φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'

LinearMap.polyCharpolyAux is independent of the choice of basis of the target module.

Proof strategy:

Rewrite polyCharpolyAux as the (honest, ordinary) characteristic polynomial of the basechange of φ to the multivariate polynomial ring MvPolynomial ι R.
Use that the characteristic polynomial of a linear map is independent of the choice of basis. This independence result is used transitively via LinearMap.polyCharpolyAux_map_aeval and LinearMap.polyCharpolyAux_map_eq_charpoly.

noncomputable def LinearMap.polyCharpoly {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) :

Polynomial (MvPolynomial ι R)

Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear family of endomorphisms. Let b be a basis of L and bₘ a basis of M. Then LinearMap.polyCharpoly φ b is the polynomial that evaluates on elements x of L to the characteristic polynomial of φ x acting on M.

Equations

φ.polyCharpoly b = φ.polyCharpolyAux b (Module.Free.chooseBasis R M)

theorem LinearMap.polyCharpoly_eq_of_basis {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [DecidableEq ιM] (bₘ : Basis ιM R M) :

φ.polyCharpoly b = Polynomial.map (↑(MvPolynomial.bind₁ (toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)

theorem LinearMap.polyCharpoly_monic {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) :

(φ.polyCharpoly b).Monic

theorem LinearMap.polyCharpoly_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [Nontrivial R] :

φ.polyCharpoly b ≠ 0

@[simp]

theorem LinearMap.polyCharpoly_natDegree {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [Nontrivial R] :

(φ.polyCharpoly b).natDegree = Module.finrank R M

theorem LinearMap.polyCharpoly_coeff_isHomogeneous {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (i j : ℕ) (hij : i + j = Module.finrank R M) [Nontrivial R] :

((φ.polyCharpoly b).coeff i).IsHomogeneous j

theorem LinearMap.polyCharpoly_baseChange {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (A : Type u_8) [CommRing A] [Algebra R A] :

(tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpoly (Algebra.TensorProduct.basis A b) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)

@[simp]

theorem LinearMap.polyCharpoly_map_eq_charpoly {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (x : L) :

Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)

@[simp]

theorem LinearMap.polyCharpoly_coeff_eval {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (x : L) (i : ℕ) :

(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (charpoly (φ x)).coeff i

theorem LinearMap.polyCharpoly_coeff_eq_zero_of_basis {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ) (H : (φ.polyCharpoly b).coeff k = 0) :

(φ.polyCharpoly b').coeff k = 0

theorem LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ) :

(φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0

noncomputable def LinearMap.nilRankAux {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (φ : L →ₗ[R] Module.End R M) (b : Basis ι R L) :

(Implementation detail, see LinearMap.nilRank.)

Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear family of endomorphisms. Then LinearMap.nilRankAux φ b is the smallest index at which LinearMap.polyCharpoly φ b has a non-zero coefficient.

This number does not depend on the choice of b, see nilRankAux_basis_indep.

Equations

φ.nilRankAux b = (φ.polyCharpoly b).natTrailingDegree

theorem LinearMap.polyCharpoly_coeff_nilRankAux_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [Nontrivial R] :

(φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0

theorem LinearMap.nilRankAux_le {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] [Module.Free R M] [Module.Finite R M] [Nontrivial R] (b : Basis ι R L) (b' : Basis ι' R L) :

φ.nilRankAux b ≤ φ.nilRankAux b'

theorem LinearMap.nilRankAux_basis_indep {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] [Module.Free R M] [Module.Finite R M] [Nontrivial R] (b : Basis ι R L) (b' : Basis ι' R L) :

φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree

noncomputable def LinearMap.nilRank {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] (φ : L →ₗ[R] Module.End R M) :

Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear family of endomorphisms. Then LinearMap.nilRank φ b is the smallest index at which LinearMap.polyCharpoly φ b has a non-zero coefficient.

This number does not depend on the choice of b, see LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree.

Equations

φ.nilRank = φ.nilRankAux (Module.Free.chooseBasis R L)

theorem LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [Nontrivial R] (b : Basis ι R L) :

φ.nilRank = (φ.polyCharpoly b).natTrailingDegree

theorem LinearMap.polyCharpoly_coeff_nilRank_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [Module.Finite R L] [Module.Free R L] [Nontrivial R] :

(φ.polyCharpoly b).coeff φ.nilRank ≠ 0

theorem LinearMap.nilRank_le_card {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [Nontrivial R] {ι : Type u_8} [Fintype ι] (b : Basis ι R M) :

φ.nilRank ≤ Fintype.card ι

theorem LinearMap.nilRank_le_finrank {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [Nontrivial R] :

φ.nilRank ≤ Module.finrank R M

theorem LinearMap.nilRank_le_natTrailingDegree_charpoly {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [Nontrivial R] (x : L) :

φ.nilRank ≤ (charpoly (φ x)).natTrailingDegree

def LinearMap.IsNilRegular {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] (x : L) :

Let L and M be finite free modules over R, and let φ : L →ₗ[R] Module.End R M be a linear family of endomorphisms, and denote n := nilRank φ.

An element x : L is nil-regular with respect to φ if the n-th coefficient of the characteristic polynomial of φ x is non-zero.

Equations

φ.IsNilRegular x = ((LinearMap.charpoly (φ x)).coeff φ.nilRank ≠ 0)

theorem LinearMap.isNilRegular_def {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] (x : L) :

φ.IsNilRegular x ↔ (charpoly (φ x)).coeff φ.nilRank ≠ 0

theorem LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [Module.Finite R L] [Module.Free R L] (x : L) :

φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0

theorem LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] (x : L) [Nontrivial R] :

φ.IsNilRegular x ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank

theorem LinearMap.exists_isNilRegular_of_finrank_le_card {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [IsDomain R] (h : ↑(Module.finrank R M) ≤ Cardinal.mk R) :

∃ (x : L), φ.IsNilRegular x

theorem LinearMap.exists_isNilRegular {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [IsDomain R] [Infinite R] :

∃ (x : L), φ.IsNilRegular x