UFD criteria via height 1 prime ideals and localization

Main results

• UniqueFactorizationMonoid.iff_height_one_primes_principal : Let R be a Noetherian domain. Then R is a UFD if and only if every height 1 prime ideal is principal.

• UniqueFactorizationMonoid.iff_localization_away_of_prime : Let R be a Noetherian domain, x ∈ R be a prime element. Then R is a UFD if and only if Rₓ is a UFD.

theorem Ideal.height_eq_zero_iff_eq_bot {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} : I.height = 0 ↔ I = ⊥

theorem Localization.Away.isDomain {R : Type u_1} [CommRing R] [IsDomain R] {x : R} (hx : x ≠ 0) : IsDomain (Away x)

If x ≠ 0, then the localization of a domain away from x is again a domain.

theorem UniqueFactorizationMonoid.height_one_primes_principal {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {p : Ideal R} [p.IsPrime] (hph : p.height = 1) : Submodule.IsPrincipal p

theorem UniqueFactorizationMonoid.of_height_one_primes_principal {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] (h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p) : UniqueFactorizationMonoid R

theorem UniqueFactorizationMonoid.iff_height_one_primes_principal {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] : UniqueFactorizationMonoid R ↔ ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p

Let R be a Noetherian domain. Then R is a UFD if and only if every height 1 prime ideal is principal.

theorem Ideal.isPrincipal_of_isPrincipal_isLocalization_away_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [WfDvdMonoid R] {x : R} (hx : Prime x) {p : Ideal R} [p.IsPrime] (hxp : x ∉ p) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.Away x S] (hp : Submodule.IsPrincipal (map (algebraMap R S) p)) : Submodule.IsPrincipal p

theorem Ideal.isPrincipal_of_isPrincipal_localization_away_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [WfDvdMonoid R] {x : R} (hx : Prime x) {p : Ideal R} [p.IsPrime] (hxp : x ∉ p) (hp : Submodule.IsPrincipal (map (algebraMap R (Localization.Away x)) p)) : Submodule.IsPrincipal p

theorem UniqueFactorizationMonoid.iff_isLocalization_away_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R} (hx : Prime x) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization.Away x S] : UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid S

theorem UniqueFactorizationMonoid.iff_localization_away_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R} (hx : Prime x) : UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid (Localization.Away x)

Let R be a Noetherian domain, x ∈ R be a prime element. Then R is a UFD if and only if Rₓ is a UFD.