A power of the image of a finitely generated ideal

Let I be an ideal of a semiring B and let f : B →+* C be a ring homomorphism into a commutative semiring. If every prime of C contains I.map f, that image lies in the nilradical of C; when I is finitely generated the image is then a nilpotent ideal, so one of its powers is ⊥.

Nothing here mentions localisation, and nothing subtracts, so the statement is made for an arbitrary ring homomorphism, with commutativity assumed only where primes are taken.

Main results

• Ideal.exists_pow_map_eq_bot: if I is finitely generated and I.map f is contained in every prime of C, then (I.map f) ^ n = ⊥ for some n.

theorem Ideal.exists_pow_map_eq_bot {B : Type u_1} {C : Type u_2} [Semiring B] [CommSemiring C] {I : Ideal B} (f : B →+* C) (hfg : I.FG) (hprime : ∀ (P : Ideal C), P.IsPrime → map f I ≤ P) : ∃ (n : ℕ), map f I ^ n = ⊥

A power of the image of I vanishes. If every prime of C contains the image of I under f, that image lies in the nilradical; being finitely generated it is then nilpotent.