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.

Example 1: A = M →ₗ[R] M, the endomorphism algebra of an R-module M.
Example 2: A = n × n matrices with entries in R.

source

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

ideal (polynomial R)

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

polynomial.ann_ideal R a = ring_hom.ker (polynomial.aeval a).to_ring_hom

source

theorem polynomial.mem_ann_ideal_iff_aeval_eq_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {a : A} {p : polynomial R} :

p ∈ polynomial.ann_ideal R a ↔ ⇑(polynomial.aeval a) p = 0

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

source

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

polynomial 𝕜

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

polynomial.ann_ideal_generator 𝕜 a = let g : polynomial 𝕜 := submodule.is_principal.generator (polynomial.ann_ideal 𝕜 a) in g * ⇑polynomial.C (g.leading_coeff)⁻¹

source

@[simp]

theorem polynomial.ann_ideal_generator_eq_zero_iff {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] {a : A} :

polynomial.ann_ideal_generator 𝕜 a = 0 ↔ polynomial.ann_ideal 𝕜 a = ⊥

source

@[simp]

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

ideal.span {polynomial.ann_ideal_generator 𝕜 a} = polynomial.ann_ideal 𝕜 a

ann_ideal_generator 𝕜 a is indeed a generator.

source

theorem polynomial.ann_ideal_generator_mem (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

polynomial.ann_ideal_generator 𝕜 a ∈ polynomial.ann_ideal 𝕜 a

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

source

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) :

p ∈ polynomial.ann_ideal 𝕜 a ↔ ∃ (s : polynomial 𝕜), p = s • polynomial.ann_ideal_generator 𝕜 a

source

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) :

(polynomial.ann_ideal_generator 𝕜 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.

source

theorem polynomial.ann_ideal_generator_aeval_eq_zero (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

⇑(polynomial.aeval a) (polynomial.ann_ideal_generator 𝕜 a) = 0

source

theorem polynomial.mem_iff_ann_ideal_generator_dvd {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] {p : polynomial 𝕜} {a : A} :

p ∈ polynomial.ann_ideal 𝕜 a ↔ polynomial.ann_ideal_generator 𝕜 a ∣ p

source

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) :

(polynomial.ann_ideal_generator 𝕜 a).degree ≤ p.degree

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

source

theorem polynomial.ann_ideal_generator_eq_minpoly (𝕜 : Type u_1) {A : Type u_2} [field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

polynomial.ann_ideal_generator 𝕜 a = minpoly 𝕜 a

The generator of the annihilating ideal is the minimal polynomial.

source

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) :

polynomial.ann_ideal_generator 𝕜 a = p

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