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 = Finset.univ.sum fun (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] : Matrix.toMvPolynomial 0 = 0

@[simp]

theorem Matrix.toMvPolynomial_one {n : Type u_2} {R : Type u_4} [Fintype n] [CommSemiring R] [DecidableEq n] : Matrix.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 : Matrix m n R) (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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R) : (MvPolynomial.eval ⇑c) (LinearMap.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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) (A : Type u_8) [CommRing A] [Algebra R A] : LinearMap.toMvPolynomial (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂) (LinearMap.baseChange A f) i = (MvPolynomial.map (algebraMap R A)) (LinearMap.toMvPolynomial b₁ b₂ f i)

theorem LinearMap.toMvPolynomial_isHomogeneous {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) : (LinearMap.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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) : (LinearMap.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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂) : MvPolynomial.constantCoeff (LinearMap.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_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : LinearMap.toMvPolynomial b₁ b₂ 0 = 0

@[simp]

theorem LinearMap.toMvPolynomial_id {R : Type u_1} {M₁ : Type u_2} {ι₁ : Type u_5} [CommRing R] [AddCommGroup M₁] [Module R M₁] [Fintype ι₁] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) : LinearMap.toMvPolynomial b₁ b₁ LinearMap.id = MvPolynomial.X

theorem LinearMap.toMvPolynomial_add {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_5} {ι₂ : Type u_6} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (g : M₁ →ₗ[R] M₂) : LinearMap.toMvPolynomial b₁ b₂ (f + g) = LinearMap.toMvPolynomial b₁ b₂ f + LinearMap.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 ι₂] [Fintype ι₃] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (b₃ : Basis ι₃ R M₃) (g : M₂ →ₗ[R] M₃) (f : M₁ →ₗ[R] M₂) (i : ι₃) : LinearMap.toMvPolynomial b₁ b₃ (g ∘ₗ f) i = (MvPolynomial.bind₁ (LinearMap.toMvPolynomial b₁ b₂ f)) (LinearMap.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] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.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ₘ) = ((LinearMap.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) = ((LinearMap.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ₘ) = LinearMap.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) = (LinearMap.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ₘ) = LinearMap.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ₘ) = ((LinearMap.tensorProduct R A M M ∘ₗ LinearMap.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:

1. Rewrite polyCharpolyAux as the (honest, ordinary) characteristic polynomial of the basechange of φ to the multivariate polynomial ring MvPolynomial ι R.
2. 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₁ (LinearMap.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 = FiniteDimensional.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 = FiniteDimensional.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] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.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) = LinearMap.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) = (LinearMap.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} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Module.Free R M] [Module.Finite R M] [Module.Finite R L] [Module.Free R L] [Nontrivial R] (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 ≤ FiniteDimensional.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 ≤ (LinearMap.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) : Prop

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 ↔ (LinearMap.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] [Nontrivial R] (x : L) : φ.IsNilRegular x ↔ (LinearMap.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] [Nontrivial R] [IsDomain R] (h : ↑(FiniteDimensional.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] [Nontrivial R] [IsDomain R] [Infinite R] : ∃ (x : L), φ.IsNilRegular x