Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Module docstring

{"# Unique factorization and ascending chain condition on ideals

Main results

Ideal.setOf_isPrincipal_wellFoundedOn_gt, WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt in a domain, well-foundedness of the strict version of ∣ is equivalent to the ascending chain condition on principal ideals. "}

Ideal.IsPrime.exists_mem_prime_of_ne_bot theorem

 {R : Type*} [CommSemiring R] [IsDomain R] [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ≠ ⊥) :
  ∃ x ∈ I, Prime x

Full source

/-- Every non-zero prime ideal in a unique factorization domain contains a prime element. -/
theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot {R : Type*} [CommSemiring R] [IsDomain R]
    [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ≠ ⊥) :
    ∃ x ∈ I, Prime x := by
  classical
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩

Existence of Prime Elements in Nonzero Prime Ideals of a UFD

Informal description

Let $R$ be a commutative semiring that is an integral domain and a unique factorization monoid. For any nonzero prime ideal $I$ of $R$, there exists a prime element $x \in I$.

Ideal.setOf_isPrincipal_wellFoundedOn_gt theorem

[CommSemiring α] [WfDvdMonoid α] [IsDomain α] : {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)

Full source

/-- The ascending chain condition on principal ideals holds in a `WfDvdMonoid` domain. -/
lemma Ideal.setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [WfDvdMonoid α] [IsDomain α] :
    {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·) := by
  have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span {a}) '' Set.univ) := by
    ext
    simp [Submodule.isPrincipal_iff, eq_comm]
  rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]
  convert wellFounded_dvdNotUnit (α := α)
  ext
  exact Ideal.span_singleton_lt_span_singleton

Well-foundedness of Strict Inclusion on Principal Ideals in a WfDvdMonoid Domain

Informal description

Let $\alpha$ be an integral domain that is a well-founded divisibility monoid. Then the set of all principal ideals in $\alpha$ is well-founded with respect to the strict inclusion relation $>$. That is, there are no infinite strictly descending chains of principal ideals in $\alpha$.

WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt theorem

[CommSemiring α] [IsDomain α] (h : {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)) : WfDvdMonoid α

Full source

/-- The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is `WfDvdMonoid`. -/
lemma WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [IsDomain α]
    (h : {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)) :
    WfDvdMonoid α := by
  have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h
  constructor
  convert InvImage.wf (fun a => ⟨Ideal.span ({a} : Set α), _, rfl⟩) this
  ext
  exact Ideal.span_singleton_lt_span_singleton.symm

Well-founded divisibility monoid from well-founded principal ideals in an integral domain

Informal description

Let $\alpha$ be an integral domain. If the set of principal ideals in $\alpha$ is well-founded with respect to the strict inclusion relation $>$, then $\alpha$ is a well-founded divisibility monoid.