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 #

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 #

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) :

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
Instances For
    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 : nR) :
    (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] :
    @[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_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
    Instances For
      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) (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_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] :
      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 : ι₂) :
      (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_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 : ι₂) :
      (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_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 (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_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₂) :
      @[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₁) :
      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_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₂) (g : M₁ →ₗ[R] M₂) :
      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 : ι₃) :
      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) :

      (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
      Instances For
        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) :

        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
        Instances For
          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 = 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] :
          (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
          Instances For
            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
            Instances For
              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 (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) :

              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
              Instances For
                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] (x : L) [Nontrivial R] :
                φ.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] [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