Localization and submonoid saturation

In this file we show that A is a localization of R on the submonoid S if and only if it is so on the saturation of S.

Crucially, the saturation of S is precisely the elements that become a unit in A.

theorem IsLocalization.mem_saturation_iff_isUnit_algebraMap {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] {x : R} : x ∈ S.saturation ↔ IsUnit ((algebraMap R A) x)

@[simp]

theorem IsLocalization.saturation_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {A : Type u_2} [CommRing A] [Algebra R A] : IsLocalization S.saturation.toSubmonoid A ↔ IsLocalization S A

theorem IsLocalization.of_saturation_eq {R : Type u_1} [CommRing R] (S T : Submonoid R) {A : Type u_2} [CommRing A] [Algebra R A] [IsLocalization S A] (ih : S.saturation = T.saturation) : IsLocalization T A

theorem IsLocalization.isLocalization_iff_of_saturation_eq {R : Type u_1} [CommRing R] (S T : Submonoid R) {A : Type u_2} [CommRing A] [Algebra R A] (ih : S.saturation = T.saturation) : IsLocalization S A ↔ IsLocalization T A

theorem IsLocalization.ext_saturation {R : Type u_1} [CommRing R] (S T : Submonoid R) {A : Type u_2} [CommRing A] [Algebra R A] [IsLocalization S A] [IsLocalization T A] : S.saturation = T.saturation