Mathlib.RingTheory.Finiteness.Ideal

Ideal.FG.map theorem

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

Full source

/-- The image of a finitely generated ideal is finitely generated.

This is the `Ideal` version of `Submodule.FG.map`. -/
theorem FG.map {R S : Type*} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) :
    (I.map f).FG := by
  classical
    obtain ⟨s, hs⟩ := h
    refine ⟨s.image f, ?_⟩
    rw [Finset.coe_image, ← Ideal.map_span, hs]

Image of a Finitely Generated Ideal under a Ring Homomorphism is Finitely Generated

Informal description

Let $R$ and $S$ be semirings, $I$ be a finitely generated ideal of $R$, and $f : R \to S$ be a ring homomorphism. Then the image ideal $f(I)$ is also finitely generated in $S$.

Ideal.fg_ker_comp theorem

 {R S A : Type*} [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

Full source

theorem fg_ker_comp {R S A : Type*} [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 := by
  letI : Algebra R S := RingHom.toAlgebra f
  letI : Algebra R A := RingHom.toAlgebra (g.comp f)
  letI : Algebra S A := RingHom.toAlgebra g
  letI : IsScalarTower R S A := IsScalarTower.of_algebraMap_eq fun _ => rfl
  let f₁ := Algebra.linearMap R S
  let g₁ := (IsScalarTower.toAlgHom R S A).toLinearMap
  exact Submodule.fg_ker_comp f₁ g₁ hf (Submodule.fg_restrictScalars (RingHom.ker g) hg hsur) hsur

Finitely Generated Kernel of Composition of Ring Homomorphisms with Surjective First Map

Informal description

Let $R$, $S$, and $A$ be commutative rings, and let $f \colon R \to S$ and $g \colon S \to A$ be ring homomorphisms. If the kernels of both $f$ and $g$ are finitely generated ideals, and $f$ is surjective, then the kernel of the composition $g \circ f$ is also a finitely generated ideal.

Ideal.exists_radical_pow_le_of_fg theorem

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

Full source

theorem exists_radical_pow_le_of_fg {R : Type*} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) :
    ∃ n : ℕ, I.radical ^ n ≤ I := by
  have := le_refl I.radical; revert this
  refine Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) ?_ ?_ _ h
  · intro x hx
    obtain ⟨n, hn⟩ := hx (subset_span (Set.mem_singleton x))
    exact ⟨n, by rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
  · intro J K hJ hK hJK
    obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| Ideal.mem_sup_left hx
    obtain ⟨m, hm⟩ := hK fun x hx => hJK <| Ideal.mem_sup_right hx
    use n + m
    rw [← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup, Finset.sup_le_iff]
    refine fun i _ => Ideal.mul_le_right.trans ?_
    obtain h | h := le_or_lt n i
    · apply Ideal.mul_le_right.trans ((Ideal.pow_le_pow_right h).trans hn)
    · apply Ideal.mul_le_left.trans
      refine (Ideal.pow_le_pow_right ?_).trans hm
      rw [add_comm, Nat.add_sub_assoc h.le]
      apply Nat.le_add_right

Existence of Power of Radical Contained in Ideal for Finitely Generated Radicals

Informal description

Let $R$ be a commutative semiring and $I$ be an ideal of $R$ whose radical $\sqrt{I}$ is finitely generated. Then there exists a natural number $n$ such that $(\sqrt{I})^n \subseteq I$.

Ideal.exists_pow_le_of_le_radical_of_fg_radical theorem

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

Full source

theorem exists_pow_le_of_le_radical_of_fg_radical {R : Type*} [CommSemiring R] {I J : Ideal R}
    (hIJ : I ≤ J.radical) (hJ : J.radical.FG) :
    ∃ k : ℕ, I ^ k ≤ J := by
  obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
  use k
  calc
    I ^ k ≤ J.radical ^ k := Ideal.pow_right_mono hIJ _
    _ ≤ J := hk

Existence of Power of Ideal Contained in Another Ideal for Finitely Generated Radicals

Informal description

Let $R$ be a commutative semiring and $I, J$ be ideals of $R$ such that $I \subseteq \sqrt{J}$ and $\sqrt{J}$ is finitely generated. Then there exists a natural number $k$ such that $I^k \subseteq J$.

Ideal.exists_pow_le_of_le_radical_of_fg theorem

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

Full source

lemma exists_pow_le_of_le_radical_of_fg {R : Type*} [CommSemiring R] {I J : Ideal R}
    (h' : I ≤ J.radical) (h : I.FG) :
    ∃ n : ℕ, I ^ n ≤ J := by
  revert h'
  apply Submodule.fg_induction _ _ _ _ _ I h
  · intro x hJ
    simp only [Ideal.submodule_span_eq, Ideal.span_le,
      Set.singleton_subset_iff, SetLike.mem_coe] at hJ
    obtain ⟨n, hn⟩ := hJ
    refine ⟨n, by simpa [Ideal.span_singleton_pow, Ideal.span_le]⟩
  · intros I₁ I₂ h₁ h₂ hJ
    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans hJ)
    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans hJ)
    use n₁ + n₂
    exact Ideal.sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Existence of Power of Finitely Generated Ideal Contained in Another Ideal

Informal description

Let $R$ be a commutative semiring, and let $I$ and $J$ be ideals of $R$ such that $I$ is finitely generated and $I \subseteq \sqrt{J}$. Then there exists a natural number $n$ such that $I^n \subseteq J$.