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} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) : Ideal (Polynomial R)

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

• Polynomial.annIdeal R a = RingHom.ker ↑(Polynomial.aeval a)

theorem Polynomial.mem_annIdeal_iff_aeval_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {p : Polynomial R} : p ∈ Polynomial.annIdeal R a ↔ (Polynomial.aeval a) 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

• Polynomial.annIdealGenerator 𝕜 a = let g := Submodule.IsPrincipal.generator (Polynomial.annIdeal 𝕜 a); g * Polynomial.C (Polynomial.leadingCoeff g)⁻¹

@[simp]

theorem Polynomial.annIdealGenerator_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {a : A} : Polynomial.annIdealGenerator 𝕜 a = 0 ↔ Polynomial.annIdeal 𝕜 a = ⊥

@[simp]

theorem Polynomial.span_singleton_annIdealGenerator (𝕜 : Type u_1) {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) : Ideal.span {Polynomial.annIdealGenerator 𝕜 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) : Polynomial.annIdealGenerator 𝕜 a ∈ Polynomial.annIdeal 𝕜 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.Monic (Polynomial.annIdealGenerator 𝕜 a)

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) : (Polynomial.aeval a) (Polynomial.annIdealGenerator 𝕜 a) = 0

theorem Polynomial.mem_iff_annIdealGenerator_dvd {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {p : Polynomial 𝕜} {a : A} : p ∈ Polynomial.annIdeal 𝕜 a ↔ Polynomial.annIdealGenerator 𝕜 a ∣ p

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.degree (Polynomial.annIdealGenerator 𝕜 a) ≤ Polynomial.degree p

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 : Polynomial.Monic p) (p_gen : Ideal.span {p} = Polynomial.annIdeal 𝕜 a) : Polynomial.annIdealGenerator 𝕜 a = p

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