Localization preserves unique factorization

Main results

• UniqueFactorizationMonoid.of_isLocalization: a localization of a unique factorization monoid is still a unique factorization monoid. In particular, a localization of a UFD is a UFD provided it is nontrivial.

theorem Submonoid.LocalizationMap.map_prime {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {S : Submonoid M} (f : S.LocalizationMap N) {m : M} (prime : Prime m) (n0 : f m ≠ 0) (nu : ¬IsUnit (f m)) : Prime (f m)

theorem Submonoid.LocalizationMap.eq_isUnit_map_mul_irreducible_of_irreducible_map {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {S : Submonoid M} [WfDvdMonoid M] (f : S.LocalizationMap N) {m : M} (hm : Irreducible (f m)) : ∃ (u : M) (m' : M), IsUnit (f u) ∧ Irreducible m' ∧ m = u * m'

theorem Submonoid.LocalizationMap.uniqueFactorizationMonoid {M : Type u_1} {N : Type u_2} [CommMonoidWithZero M] [CommMonoidWithZero N] {S : Submonoid M} (f : S.LocalizationMap N) [UniqueFactorizationMonoid M] : UniqueFactorizationMonoid N

theorem UniqueFactorizationMonoid.of_isLocalization {M : Type u_1} [CommSemiring M] (S : Submonoid M) (N : Type u_3) [CommSemiring N] [Algebra M N] [IsLocalization S N] [UniqueFactorizationMonoid M] : UniqueFactorizationMonoid N

A localization of a unique factorization monoid is still a unique factorization monoid.

instance instUniqueFactorizationMonoidLocalization {M : Type u_1} [CommSemiring M] (S : Submonoid M) [UniqueFactorizationMonoid M] : UniqueFactorizationMonoid (Localization S)