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

.

`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

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

`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

`annIdealGenerator 𝕜 a`

is indeed a generator.

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.