Unique factorization and ascending chain condition on ideals #
Main results #
Ideal.setOf_isPrincipal_wellFoundedOn_gt,WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gtin a domain, well-foundedness of the strict version of ∣ is equivalent to the ascending chain condition on principal ideals.
theorem
Ideal.IsPrime.exists_mem_prime_of_ne_bot
{R : Type u_2}
[CommSemiring R]
[IsDomain R]
[UniqueFactorizationMonoid R]
{I : Ideal R}
(hI₂ : I.IsPrime)
(hI : I ≠ ⊥)
:
∃ x ∈ I, Prime x
Every non-zero prime ideal in a unique factorization domain contains a prime element.
theorem
Ideal.setOf_isPrincipal_wellFoundedOn_gt
{α : Type u_1}
[CommSemiring α]
[WfDvdMonoid α]
[IsDomain α]
:
{I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2
The ascending chain condition on principal ideals holds in a WfDvdMonoid domain.
theorem
WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt
{α : Type u_1}
[CommSemiring α]
[IsDomain α]
(h : {I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2)
:
The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is WfDvdMonoid.