Localisation of a UFD at one element

If R is a UFD and y is a nonzero element, then R[y^{-1}] is again a UFD. The prime factors of any numerator that are associate to y become units in the localisation the remaining irreducibles stay prime.

theorem prime_algebraMap_of_not_dvd_pow {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] (y p : R₀) (hp : Prime p) (hpy : ∀ (n : ℕ), ¬p ∣ y ^ n) : Prime ((algebraMap R₀ (Localization.Away y)) p)

A prime element p that doesn't divide any power of y stays prime in R[y⁻¹].

theorem localization_away_UFD {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] [UniqueFactorizationMonoid R₀] (y : R₀) (hy : y ≠ 0) : UniqueFactorizationMonoid (Localization.Away y)

In a UFD, the localization away from a nonzero element is a UFD.

theorem localization_submonoid_UFD {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] [UniqueFactorizationMonoid R₀] {S : Type u_2} [CommRing S] [Algebra R₀ S] {M : Submonoid R₀} [IsLocalization M S] (hM : M ≤ nonZeroDivisors R₀) : UniqueFactorizationMonoid S

In a UFD, the localization at any submonoid of non-zero-divisors is a UFD. Generalizes localization_away_UFD to an arbitrary submonoid M.