Transport of ideals along ring homomorphisms

Taking radicals before extending an ideal does not change the radical of its extension. Powers of ideals commute with pullback along a ring equivalence, a ring homomorphism carrying I into J carries each power of I into the same power of J, and extension along a bijective ring homomorphism preserves and reflects primality. Extension preserves coprimality to an ideal whose contraction is coprime to the original ideal. Extending an ideal to an algebra and then along an algebra homomorphism is extending it directly. An algebra equivalence transports a principal ideal to the ideal generated by the transported element, and its annihilator to the annihilator of that ideal. The principal-ideal result applies to ideals extended from a common commutative semiring, without assuming the algebras commutative.

If t ∈ I and r • I ≤ (t), then I extends to the principal ideal (f t) along every ring homomorphism f for which f r is a unit.

@[simp]

theorem Ideal.radical_map_radical {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [CommSemiring S] [FunLike F R S] [RingHomClass F R S] (I : Ideal R) (f : F) : (map f I.radical).radical = (map f I).radical

Taking the radical before extending an ideal does not change the radical of its extension.

@[simp]

theorem Ideal.comap_pow_of_ringEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (I : Ideal R) (e : S ≃+* R) (n : ℕ) : comap e (I ^ n) = comap e I ^ n

Pullback along a ring equivalence commutes with powers of ideals.

theorem Ideal.isPrime_map_iff_of_bijective {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Bijective ⇑f) {I : Ideal R} : (map f I).IsPrime ↔ I.IsPrime

Extension along a bijective ring homomorphism preserves and reflects primality; compare Ideal.isMaximal_map_iff_of_bijective.

theorem Ideal.map_sup_eq_top_of_coprime_comap {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] {f : F} {I : Ideal R} {J : Ideal S} (h : I ⊔ comap f J = ⊤) : map f I ⊔ J = ⊤

Extension preserves coprimality: if I is coprime to the contraction of J, then the extension of I is coprime to J.

@[simp]

theorem Ideal.map_map_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) (I : Ideal R) : map φ (map (algebraMap R A) I) = map (algebraMap R B) I

Extending an ideal of R to an R-algebra A and then along an R-algebra homomorphism A → B gives its extension to B.

theorem Ideal.map_mem_pow_of_le_comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) {I : Ideal R} {J : Ideal S} (h : I ≤ comap f J) {n : ℕ} {x : R} (hx : x ∈ I ^ n) : f x ∈ J ^ n

A ring homomorphism f with I ≤ J.comap f maps I ^ n into J ^ n.

theorem Ideal.map_eq_span_singleton_of_isUnit {B : Type u_1} {B' : Type u_2} {F : Type u_3} [CommSemiring B] [Semiring B'] [FunLike F B B'] [RingHomClass F B B'] (f : F) {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 AlgEquiv.map_eq_span_singleton_and_annihilator {A : Type u_1} {L : Type u_2} {L' : Type u_3} [CommSemiring A] [Semiring L] [Semiring L'] [Algebra A L] [Algebra A L'] (e : L ≃ₐ[A] L') {𝔞 𝔟 : Ideal A} {a' : L'} (h𝔞 : Ideal.map (algebraMap A L') 𝔞 = Ideal.span {a'}) (h𝔟 : Ideal.map (algebraMap A L') 𝔟 = Submodule.annihilator (Ideal.span {a'})) : Ideal.map (algebraMap A L) 𝔞 = Ideal.span {e.symm a'} ∧ Ideal.map (algebraMap A L) 𝔟 = Submodule.annihilator (Ideal.span {e.symm a'})

If the extensions of two ideals to L' are a principal ideal and its annihilator, the extensions to an equivalent A-algebra L have the same form.