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.

• Example 1: A = M โโ[R] M, the endomorphism algebra of an R-module M.
• Example 2: A = n ร n matrices with entries in R.
noncomputable def Polynomial.annIdeal (R : Type u_1) {A : Type u_2} [] [] [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
theorem Polynomial.mem_annIdeal_iff_aeval_eq_zero {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {a : A} {p : } :
โ p = 0

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) :
= Polynomial.annIdeal ๐ 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 โข
theorem Polynomial.monic_annIdealGenerator (๐ : Type u_1) {A : Type u_2} [Field ๐] [Ring A] [Algebra ๐ A] (a : A) (hg : โ  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) :
= 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) :
= p

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} [] [Module ๐ M] (f : Module.End ๐ M) :
Ideal.span {minpoly ๐ f} = Module.annihilator (Polynomial ๐)