English
For a ring R, an algebra A over R and an element a in A, the annihilating ideal annIdeal_R(a) consists of all polynomials p in R[X] such that p(a) = 0; equivalently annIdeal_R(a) = ker (aeval_a : R[X] → A).
Русский
Для кольца R, алгебры A над R и элемента a в A, аннигилирующий идеал annIdeal_R(a) состоит из всех многочленов p в R[X], таких что p(a) = 0; эквивалентно annIdeal_R(a) = ker (aeval_a : R[X] → A).
LaTeX
$$$\operatorname{annIdeal}_R(a) = \ker\big(\mathrm{aeval}_a : R[X] \to A\big)$$$
Lean4
/-- `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. -/
noncomputable def annIdeal (a : A) : Ideal R[X] :=
RingHom.ker ((aeval a).toRingHom : R[X] →+* A)
