Documentation

Mathlib.LinearAlgebra.AnnihilatingPolynomial

Annihilating Ideal #

Given a commutative ring R and an R-algebra A Every element a : A defines an ideal Polynomial.annIdeal a โŠ† R[X]. Simply put, this is the set of polynomials p where the polynomial evaluation p(a) is 0.

Special case where the ground ring is a field #

In the special case that R is a field, we use the notation R = ๐•œ. Here ๐•œ[X] is a PID, so there is a polynomial g โˆˆ Polynomial.annIdeal a which generates the ideal. We show that if this generator is chosen to be monic, then it is the minimal polynomial of a, as defined in FieldTheory.Minpoly.

Special case: endomorphism algebra #

Given an R-module M ([AddCommGroup M] [Module R M]) there are some common specializations which may be more familiar.

noncomputable def Polynomial.annIdeal (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

annIdeal R a is the annihilating ideal of all p : R[X] such that p(a) = 0.

The informal notation p(a) stand for Polynomial.aeval a p. Again informally, the annihilating ideal of a is { p โˆˆ R[X] | p(a) = 0 }. This is an ideal in R[X]. The formal definition uses the kernel of the aeval map.

Equations
Instances For

    It is useful to refer to ideal membership sometimes and the annihilation condition other times.

    noncomputable def Polynomial.annIdealGenerator (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) :
    Polynomial ๐•œ

    annIdealGenerator ๐•œ a is the monic generator of annIdeal ๐•œ a if one exists, otherwise 0.

    Since ๐•œ[X] is a principal ideal domain there is a polynomial g such that span ๐•œ {g} = annIdeal a. This picks some generator. We prefer the monic generator of the ideal.

    Equations
    Instances For
      @[simp]
      theorem Polynomial.annIdealGenerator_eq_zero_iff {๐•œ : Type u_1} {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] {a : A} :
      @[simp]
      theorem Polynomial.span_singleton_annIdealGenerator (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) :

      annIdealGenerator ๐•œ a is indeed a generator.

      theorem Polynomial.annIdealGenerator_mem (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) :

      The annihilating ideal generator is a member of the annihilating ideal.

      theorem Polynomial.mem_iff_eq_smul_annIdealGenerator (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] {p : Polynomial ๐•œ} (a : A) :
      p โˆˆ Polynomial.annIdeal ๐•œ a โ†” โˆƒ (s : Polynomial ๐•œ), p = s โ€ข Polynomial.annIdealGenerator ๐•œ a
      theorem Polynomial.monic_annIdealGenerator (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) (hg : Polynomial.annIdealGenerator ๐•œ a โ‰  0) :
      (Polynomial.annIdealGenerator ๐•œ a).Monic

      The generator we chose for the annihilating ideal is monic when the ideal is non-zero.

      We are working toward showing the generator of the annihilating ideal in the field case is the minimal polynomial. We are going to use a uniqueness theorem of the minimal polynomial.

      This is the first condition: it must annihilate the original element a : A.

      theorem Polynomial.annIdealGenerator_aeval_eq_zero (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) :
      theorem Polynomial.mem_iff_annIdealGenerator_dvd {๐•œ : Type u_1} {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] {p : Polynomial ๐•œ} {a : A} :
      theorem Polynomial.degree_annIdealGenerator_le_of_mem {๐•œ : Type u_1} {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) (p : Polynomial ๐•œ) (hp : p โˆˆ Polynomial.annIdeal ๐•œ a) (hpn0 : p โ‰  0) :
      (Polynomial.annIdealGenerator ๐•œ a).degree โ‰ค p.degree

      The generator of the annihilating ideal has minimal degree among the non-zero members of the annihilating ideal

      theorem Polynomial.annIdealGenerator_eq_minpoly (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) :
      Polynomial.annIdealGenerator ๐•œ a = minpoly ๐•œ a

      The generator of the annihilating ideal is the minimal polynomial.

      theorem Polynomial.monic_generator_eq_minpoly (๐•œ : Type u_1) {A : Type u_2} [Field ๐•œ] [Ring A] [Algebra ๐•œ A] (a : A) (p : Polynomial ๐•œ) (p_monic : p.Monic) (p_gen : Ideal.span {p} = Polynomial.annIdeal ๐•œ a) :

      If a monic generates the annihilating ideal, it must match our choice of the annihilating ideal generator.

      theorem Polynomial.span_minpoly_eq_annihilator (๐•œ : Type u_1) [Field ๐•œ] {M : Type u_3} [AddCommGroup M] [Module ๐•œ M] (f : Module.End ๐•œ M) :