Ideals that become principal in an away localization

If r • I ≤ (t) for an element t of an ideal I, then I and (t) agree after inverting r. This is how a local equation of an ideal is read off from a relation holding up to a multiplier, as produced by Nakayama's lemma.

Main results

• Ideal.map_eq_span_singleton_of_isUnit: if f r is a unit for a ring homomorphism f, then r • I ≤ (t) and t ∈ I imply that I generates (f t) after applying f.
• Ideal.map_algebraMap_away_eq_span_singleton: if r • I ≤ (t) and t ∈ I, then I generates (t) in the localization away from r.

theorem Ideal.map_eq_span_singleton_of_isUnit {B : Type u_1} {B' : Type u_2} [CommSemiring B] [CommSemiring B'] (f : B →+* B') {I : Ideal B} {r t : B} (ht : t ∈ I) (h : r • I ≤ span {t}) (hr : IsUnit (f r)) : map f I = span {f t}

If f r is a unit, r • I ≤ (t), and t ∈ I, then I generates the principal ideal (f t) after applying the ring homomorphism f.

theorem Ideal.map_algebraMap_away_eq_span_singleton {B : Type u_1} {B' : Type u_2} [CommSemiring B] [CommSemiring B'] [Algebra B B'] {I : Ideal B} {r t : B} [IsLocalization.Away r B'] (ht : t ∈ I) (h : r • I ≤ span {t}) : map (algebraMap B B') I = span {(algebraMap B B') t}

If r • I ≤ (t) for some t ∈ I, then I generates the principal ideal (t) in the localization away from r.