# 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.

• 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.

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 ↑() 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} [] [Ring A] [Algebra 𝕜 A] (a : A) :

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.

Instances For
@[simp]
theorem Polynomial.annIdealGenerator_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] {a : A} :
@[simp]
theorem Polynomial.span_singleton_annIdealGenerator (𝕜 : Type u_1) {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] (a : A) :

annIdealGenerator 𝕜 a is indeed a generator.

theorem Polynomial.annIdealGenerator_mem (𝕜 : Type u_1) {A : Type u_2} [] [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} [] [Ring A] [Algebra 𝕜 A] {p : } (a : A) :
p s, p =
theorem Polynomial.monic_annIdealGenerator (𝕜 : Type u_1) {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] (a : A) (hg : ) :

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} [] [Ring A] [Algebra 𝕜 A] (a : A) :
↑() () = 0
theorem Polynomial.mem_iff_annIdealGenerator_dvd {𝕜 : Type u_1} {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] {p : } {a : A} :
p
theorem Polynomial.degree_annIdealGenerator_le_of_mem {𝕜 : Type u_1} {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] (a : A) (p : ) (hp : p ) (hpn0 : p 0) :

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} [] [Ring A] [Algebra 𝕜 A] (a : A) :

The generator of the annihilating ideal is the minimal polynomial.

theorem Polynomial.monic_generator_eq_minpoly (𝕜 : Type u_1) {A : Type u_2} [] [Ring A] [Algebra 𝕜 A] (a : A) (p : ) (p_monic : ) (p_gen : Ideal.span {p} = ) :

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