Finitely generated ideals

Lemmas about finiteness of ideal operations.

theorem Ideal.FG.map {R : Type u_3} {S : Type u_4} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) : (Ideal.map f I).FG

The image of a finitely generated ideal is finitely generated.

This is the Ideal version of Submodule.FG.map.

theorem Ideal.fg_ker_comp {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [CommRing A] (f : R →+* S) (g : S →+* A) (hf : (RingHom.ker f).FG) (hg : (RingHom.ker g).FG) (hsur : Function.Surjective ⇑f) : (RingHom.ker (g.comp f)).FG

theorem Ideal.fg_of_fg_map_of_fg_inf_ker_of_surjective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} {I : Ideal R} (hmap : (map f I).FG) (hk : (I ⊓ RingHom.ker f).FG) (hf : Function.Surjective ⇑f) : I.FG

Let f : R →+* S be a surjective ring homomorphism, and let I be an ideal of R. If f(I) and I ∩ ker(f) are finitely generated ideals, then I is also finitely generated.

theorem Ideal.exists_radical_pow_le_of_fg {R : Type u_3} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) : ∃ (n : ℕ), I.radical ^ n ≤ I

theorem Ideal.exists_pow_le_of_le_radical_of_fg_radical {R : Type u_3} [CommSemiring R] {I J : Ideal R} (hIJ : I ≤ J.radical) (hJ : J.radical.FG) : ∃ (k : ℕ), I ^ k ≤ J

theorem Ideal.exists_pow_le_of_le_radical_of_fg {R : Type u_3} [CommSemiring R] {I J : Ideal R} (h' : I ≤ J.radical) (h : I.FG) : ∃ (n : ℕ), I ^ n ≤ J

theorem Submodule.FG.smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {I : Ideal R} [I.IsTwoSided] {N : Submodule R M} (hI : I.FG) (hN : N.FG) : (I • N).FG

theorem Ideal.FG.mul {R : Type u_1} [Semiring R] {I J : Ideal R} [I.IsTwoSided] (hI : I.FG) (hJ : J.FG) : (I * J).FG

theorem Ideal.FG.pow {R : Type u_1} [Semiring R] {I : Ideal R} [I.IsTwoSided] {n : ℕ} (hI : I.FG) : (I ^ n).FG