Annihilating Ideal #
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 anR
-module M. - Example 2:
A = n × n
matrices with entries inR
.
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.
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)⁻¹
ann_ideal_generator 𝕜 a
is indeed a generator.
The annihilating ideal generator is a member of the annihilating ideal.
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
.
The generator of the annihilating ideal has minimal degree among the non-zero members of the annihilating ideal
The generator of the annihilating ideal is the minimal polynomial.
If a monic generates the annihilating ideal, it must match our choice of the annihilating ideal generator.