mathlib3 documentation

linear_algebra.annihilating_polynomial

Annihilating Ideal #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a commutative ring R and an R-algebra A Every element a : A defines an ideal polynomial.ann_ideal 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.ann_ideal 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 field_theory.minpoly.

Special case: endomorphism algebra #

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

noncomputable def polynomial.ann_ideal (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) :

ann_ideal 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

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

noncomputable def polynomial.ann_ideal_generator (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

ann_ideal_generator 𝕜 a is the monic generator of ann_ideal 𝕜 a if one exists, otherwise 0.

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

Equations
@[simp]
theorem polynomial.ann_ideal_generator_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] {a : A} :
@[simp]
theorem polynomial.span_singleton_ann_ideal_generator (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

ann_ideal_generator 𝕜 a is indeed a generator.

theorem polynomial.ann_ideal_generator_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_ann_ideal_generator (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] {p : polynomial 𝕜} (a : A) :
theorem polynomial.monic_ann_ideal_generator (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) (hg : polynomial.ann_ideal_generator 𝕜 a 0) :

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.ann_ideal_generator_aeval_eq_zero (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :
theorem polynomial.mem_iff_ann_ideal_generator_dvd {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] {p : polynomial 𝕜} {a : A} :
theorem polynomial.degree_ann_ideal_generator_le_of_mem {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) (p : polynomial 𝕜) (hp : p polynomial.ann_ideal 𝕜 a) (hpn0 : p 0) :

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

theorem polynomial.ann_ideal_generator_eq_minpoly (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [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} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) (p : polynomial 𝕜) (p_monic : p.monic) (p_gen : ideal.span {p} = polynomial.ann_ideal 𝕜 a) :

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