UFD criteria via height 1 prime ideals and localization

Main results

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

• UniqueFactorizationMonoid.iff_localizationAway_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.isPrincipal_of_isPrincipal_isLocalizationAway_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_localizationAway_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.isPrincipal_of_height_eq_one {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_forall_isPrincipal_of_height_eq_one {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_forall_isPrincipal_of_height_eq_one {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 UniqueFactorizationMonoid.iff_of_isLocalizationAway_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_localizationAway_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.