A fraction ring of a localization is a fraction ring of the base

Let S be the localization of a ring R at a submonoid M of non-zero-divisors. A total ring of fractions T of S is then a total ring of fractions of R (TauCeti.IsFractionRing.of_isLocalization_of_isFractionRing). Mathlib proves the converse direction, from a fraction ring of R to one of S, as IsFractionRing.isFractionRing_of_isLocalization. This lets a statement about the fraction field of a localization of a domain be reduced to the fraction field of the domain itself. The non-zero-divisor hypothesis holds whenever a domain is localized to a nontrivial ring (TauCeti.IsLocalization.le_nonZeroDivisors_of_nontrivial).

An injective ring homomorphism that carries non-zero-divisors to non-zero-divisors induces an injective map of total rings of fractions (IsLocalization.map_injective_of_injective_of_le_nonZeroDivisors), with no domain hypothesis.

When every positive integer is a non-zero-divisor of R, every quotient of a total ring of fractions of R by a proper ideal has characteristic zero (IsFractionRing.charZero_quotient).

theorem TauCeti.IsLocalization.le_nonZeroDivisors_of_nontrivial {R : Type u_1} [CommRing R] [NoZeroDivisors R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Nontrivial S] [Algebra R S] [IsLocalization M S] : M ≤ nonZeroDivisors R

A submonoid of a ring without zero divisors along which the ring localizes to a nontrivial ring consists of non-zero-divisors.

theorem IsLocalization.map_injective_of_injective_of_le_nonZeroDivisors {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {M : Submonoid R} {T : Submonoid S} (Rₘ : Type u_3) (Sₘ : Type u_4) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [Algebra S Sₘ] [IsLocalization M Rₘ] [IsLocalization T Sₘ] {f : R →+* S} (hf : Function.Injective ⇑f) (hMT : M ≤ Submonoid.comap f T) (hT : T ≤ nonZeroDivisors S) : Function.Injective ⇑(map Sₘ f hMT)

Let f : R →+* S be injective, carrying a submonoid M into a submonoid T of non-zero-divisors of S. Then the induced map from the localization of R at M to that of S at T is injective. Unlike IsLocalization.map_injective_of_injective', S need not be a domain; the main case is the induced map of total quotient rings, M = R⁰ and T = S⁰.

theorem TauCeti.IsFractionRing.of_isLocalization_of_isFractionRing {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) (T : Type u_3) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing S T] (hM : M ≤ nonZeroDivisors R) : IsFractionRing R T

If S is the localization of R at a submonoid M of non-zero-divisors, then a total ring of fractions of S is a total ring of fractions of R.

theorem IsFractionRing.charZero_quotient (A : Type u_1) (K : Type u_2) [CommRing A] [CommRing K] [Algebra A K] [IsFractionRing A K] (h : ∀ (n : ℕ), n ≠ 0 → ↑n ∈ nonZeroDivisors A) {I : Ideal K} (hI : I ≠ ⊤) : CharZero (K ⧸ I)

If every positive integer is a non-zero-divisor of A, then every quotient of the total quotient ring of A by a proper ideal has characteristic zero.