Ideals together with their annihilators

In a reduced Noetherian ring, an ideal J and its annihilator together contain a nonzerodivisor. An element killing J.annihilator ⊔ J lies in J.annihilator and kills itself, so it is nilpotent, hence zero; Mathlib's IsSMulRegular.subsingleton_linearMap_iff turns this into a regular element of J.annihilator ⊔ J.

This is the input that splits an idempotent off the total ring of fractions of a reduced Noetherian ring with two minimal primes, as in IsLocalRing.isDomain_of_isIntegrallyClosed.

Main results

• Ideal.exists_mem_annihilator_sup_isSMulRegular: in a reduced Noetherian ring, every ideal together with its annihilator contains a nonzerodivisor.

theorem Ideal.exists_mem_annihilator_sup_isSMulRegular {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsReduced R] (J : Ideal R) : ∃ b ∈ Submodule.annihilator J ⊔ J, IsSMulRegular R b

In a reduced Noetherian ring, every ideal J together with its annihilator contains a nonzerodivisor: some element of J.annihilator ⊔ J is regular on R.