The radical of a principal ideal #
In a principal ideal domain R, both R and its monoid of ideals are unique factorisation
monoids, so each has a radical UniqueFactorizationMonoid.radical, the product of the distinct
normalised prime factors. This file proves that the two radicals correspond under
x ↦ Ideal.span {x}:
radical (Ideal.span {x}) = Ideal.span {radical x}.
Ideal-valued invariants over a Dedekind domain, such as the radical of a discriminant or
conductor ideal, can therefore be read as elements once the ring is principal, for instance
over ℤ. Mathlib's Ideal.radical_span_singleton_eq_span_radical is the analogous statement
for the ideal-theoretic radical Ideal.radical.
Main results #
UniqueFactorizationMonoid.radical_span_singleton: in a principal ideal domain,radical (Ideal.span {x}) = Ideal.span {radical x}.
In a principal ideal domain, the radical of a principal ideal is generated by the radical
of its generator. Both radicals are taken in the sense of UniqueFactorizationMonoid.radical,
on the left in the monoid of ideals and on the right in R.