Localizations of commutative rings

We characterize the localization of a commutative ring R at a submonoid M up to isomorphism; that is, a commutative ring S is the localization of R at M iff we can find a ring homomorphism f : R →+* S satisfying 3 properties:

1. For all y ∈ M, f y is a unit;
2. For all z : S, there exists (x, y) : R × M such that z * f y = f x;
3. For all x, y : R such that f x = f y, there exists c ∈ M such that x * c = y * c. (The converse is a consequence of 1.)

In the following, let R, P be commutative rings, S, Q be R- and P-algebras and M, T be submonoids of R and P respectively, e.g.:

variable (R S P Q : Type*) [CommRing R] [CommRing S] [CommRing P] [CommRing Q]
variable [Algebra R S] [Algebra P Q] (M : Submonoid R) (T : Submonoid P)

Main definitions

• IsLocalization (M : Submonoid R) (S : Type*) is a typeclass expressing that S is a localization of R at M, i.e. the canonical map algebraMap R S : R →+* S is a localization map (satisfying the above properties).
• IsLocalization.mk' S is a surjection sending (x, y) : R × M to f x * (f y)⁻¹
• IsLocalization.lift is the ring homomorphism from S induced by a homomorphism from R which maps elements of M to invertible elements of the codomain.
• IsLocalization.map S Q is the ring homomorphism from S to Q which maps elements of M to elements of T
• IsLocalization.ringEquivOfRingEquiv: if R and P are isomorphic by an isomorphism sending M to T, then S and Q are isomorphic

Main results

• Localization M S, a construction of the localization as a quotient type, defined in GroupTheory.MonoidLocalization, has CommRing, Algebra R and IsLocalization M instances if R is a ring. Localization.Away, Localization.AtPrime and FractionRing are abbreviations for Localizations and have their corresponding IsLocalization instances

Implementation notes

In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite one structure with an isomorphic one; one way around this is to isolate a predicate characterizing a structure up to isomorphism, and reason about things that satisfy the predicate.

A previous version of this file used a fully bundled type of ring localization maps, then used a type synonym f.codomain for f : LocalizationMap M S to instantiate the R-algebra structure on S. This results in defining ad-hoc copies for everything already defined on S. By making IsLocalization a predicate on the algebraMap R S, we can ensure the localization map commutes nicely with other algebraMaps.

To prove most lemmas about a localization map algebraMap R S in this file we invoke the corresponding proof for the underlying CommMonoid localization map IsLocalization.toLocalizationMap M S, which can be found in GroupTheory.MonoidLocalization and the namespace Submonoid.LocalizationMap.

To reason about the localization as a quotient type, use mk_eq_of_mk' and associated lemmas. These show the quotient map mk : R → M → Localization M equals the surjection LocalizationMap.mk' induced by the map algebraMap : R →+* Localization M. The lemma mk_eq_of_mk' hence gives you access to the results in the rest of the file, which are about the LocalizationMap.mk' induced by any localization map.

The proof that "a CommRing K which is the localization of an integral domain R at R \ {0} is a field" is a def rather than an instance, so if you want to reason about a field of fractions K, assume [Field K] instead of just [CommRing K].

Tags

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

class IsLocalization {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] : Prop

The typeclass IsLocalization (M : Submonoid R) S where S is an R-algebra expresses that S is isomorphic to the localization of R at M.

• map_units' (y : ↥M) : IsUnit ((algebraMap R S) ↑y)

  Everything in the image of algebraMap is a unit

• surj' (z : S) : ∃ (x : R × ↥M), z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

  The algebraMap is surjective

• exists_of_eq {x y : R} : (algebraMap R S) x = (algebraMap R S) y → ∃ (c : ↥M), ↑c * x = ↑c * y

  The kernel of algebraMap is contained in the annihilator of M; it is then equal to the annihilator by map_units'

theorem isLocalization_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] : IsLocalization M S ↔ (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧ (∀ (z : S), ∃ (x : R × ↥M), z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧ ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ (c : ↥M), ↑c * x = ↑c * y

theorem IsLocalization.map_units {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (y : ↥M) : IsUnit ((algebraMap R S) ↑y)

Everything in the image of algebraMap is a unit

theorem IsLocalization.surj {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : ∃ (x : R × ↥M), z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

The algebraMap is surjective

theorem IsLocalization.eq_iff_exists {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x y : R} : (algebraMap R S) x = (algebraMap R S) y ↔ ∃ (c : ↥M), ↑c * x = ↑c * y

The kernel of algebraMap is contained in the annihilator of M; it is then equal to the annihilator by map_units'

theorem IsLocalization.injective_iff_isRegular {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] : Function.Injective ⇑(algebraMap R S) ↔ ∀ (c : ↥M), IsRegular ↑c

theorem IsLocalization.of_le {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)) : IsLocalization N S

theorem IsLocalization.of_le_of_exists_dvd {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) : IsLocalization N S

theorem IsLocalization.algebraMap_isUnit_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} : IsUnit ((algebraMap R S) x) ↔ ∃ m ∈ M, x ∣ m

def IsLocalization.toLocalizationWithZeroMap {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : M.LocalizationWithZeroMap S

IsLocalization.toLocalizationWithZeroMap M S shows S is the monoid localization of R at M.

Equations

• IsLocalization.toLocalizationWithZeroMap M S = { toFun := ⇑(algebraMap R S), map_one' := ⋯, map_mul' := ⋯, map_units' := ⋯, surj' := ⋯, exists_of_eq := ⋯, map_zero' := ⋯ }

@[simp]

theorem IsLocalization.toLocalizationWithZeroMap_toFun {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : R) : (↑(toLocalizationWithZeroMap M S).toMonoidHom).toFun a = (algebraMap R S) a

@[reducible, inline]

abbrev IsLocalization.toLocalizationMap {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : M.LocalizationMap S

IsLocalization.toLocalizationMap M S shows S is the monoid localization of R at M.

Equations

• IsLocalization.toLocalizationMap M S = (IsLocalization.toLocalizationWithZeroMap M S).toLocalizationMap

@[simp]

theorem IsLocalization.toLocalizationMap_toMap {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : (toLocalizationMap M S).toMap = ↑↑(algebraMap R S)

theorem IsLocalization.toLocalizationMap_toMap_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) : (toLocalizationMap M S).toMap x = (algebraMap R S) x

theorem IsLocalization.surj₂ {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (z w : S) : ∃ (z' : R) (w' : R) (d : ↥M), z * (algebraMap R S) ↑d = (algebraMap R S) z' ∧ w * (algebraMap R S) ↑d = (algebraMap R S) w'

noncomputable def IsLocalization.sec {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : R × ↥M

Given a localization map f : M →* N, a section function sending z : N to some (x, y) : M × S such that f x * (f y)⁻¹ = z.

Equations

• IsLocalization.sec M z = Classical.choose ⋯

@[simp]

theorem IsLocalization.toLocalizationMap_sec {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] : (toLocalizationMap M S).sec = sec M

theorem IsLocalization.sec_spec {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : z * (algebraMap R S) ↑(sec M z).2 = (algebraMap R S) (sec M z).1

Given z : S, IsLocalization.sec M z is defined to be a pair (x, y) : R × M such that z * f y = f x (so this lemma is true by definition).

theorem IsLocalization.sec_spec' {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : (algebraMap R S) (sec M z).1 = (algebraMap R S) ↑(sec M z).2 * z

Given z : S, IsLocalization.sec M z is defined to be a pair (x, y) : R × M such that z * f y = f x, so this lemma is just an application of S's commutativity.

theorem IsLocalization.subsingleton {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (h : 0 ∈ M) : Subsingleton S

If M contains 0 then the localization at M is trivial.

theorem IsLocalization.subsingleton_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] : Subsingleton S ↔ 0 ∈ M

theorem IsLocalization.map_right_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x y : R} {c : ↥M} (h : (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y)) : (algebraMap R S) x = (algebraMap R S) y

theorem IsLocalization.map_left_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x y : R} {c : ↥M} (h : (algebraMap R S) (x * ↑c) = (algebraMap R S) (y * ↑c)) : (algebraMap R S) x = (algebraMap R S) y

theorem IsLocalization.eq_zero_of_fst_eq_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {z : S} {x : R} {y : ↥M} (h : z * (algebraMap R S) ↑y = (algebraMap R S) x) (hx : x = 0) : z = 0

theorem IsLocalization.map_eq_zero_iff {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (r : R) : (algebraMap R S) r = 0 ↔ ∃ (m : ↥M), ↑m * r = 0

noncomputable def IsLocalization.mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : S

IsLocalization.mk' S is the surjection sending (x, y) : R × M to f x * (f y)⁻¹.

Equations

• IsLocalization.mk' S x y = (IsLocalization.toLocalizationMap M S).mk' x y

@[simp]

theorem IsLocalization.mk'_sec {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : mk' S (sec M z).1 (sec M z).2 = z

theorem IsLocalization.mk'_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : ↥M) : mk' S (x₁ * x₂) (y₁ * y₂) = mk' S x₁ y₁ * mk' S x₂ y₂

theorem IsLocalization.mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) : mk' S x 1 = (algebraMap R S) x

@[simp]

theorem IsLocalization.mk'_spec {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : mk' S x y * (algebraMap R S) ↑y = (algebraMap R S) x

@[simp]

theorem IsLocalization.mk'_spec' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : (algebraMap R S) ↑y * mk' S x y = (algebraMap R S) x

@[simp]

theorem IsLocalization.mk'_spec_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (hy : y ∈ M) : mk' S x ⟨y, hy⟩ * (algebraMap R S) y = (algebraMap R S) x

@[simp]

theorem IsLocalization.mk'_spec'_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (hy : y ∈ M) : (algebraMap R S) y * mk' S x ⟨y, hy⟩ = (algebraMap R S) x

theorem IsLocalization.eq_mk'_iff_mul_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} {z : S} : z = mk' S x y ↔ z * (algebraMap R S) ↑y = (algebraMap R S) x

theorem IsLocalization.eq_mk'_of_mul_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} {z : R} (h : z * ↑y = x) : (algebraMap R S) z = mk' S x y

theorem IsLocalization.mk'_eq_iff_eq_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} {z : S} : mk' S x y = z ↔ (algebraMap R S) x = z * (algebraMap R S) ↑y

theorem IsLocalization.mk'_add_eq_iff_add_mul_eq_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} {z₁ z₂ : S} : mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

theorem IsLocalization.mk'_pow {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) (n : ℕ) : mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

theorem IsLocalization.mk'_surjective {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) : ∃ (x : R) (y : ↥M), mk' S x y = z

noncomputable def IsLocalization.fintype' {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] [Fintype R] : Fintype S

The localization of a Fintype is a Fintype. Cannot be an instance.

Equations

• IsLocalization.fintype' M S = Fintype.ofSurjective (Function.uncurry (IsLocalization.mk' S)) ⋯

def IsLocalization.uniqueOfZeroMem {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (h : 0 ∈ M) : Unique S

Localizing at a submonoid with 0 inside it leads to the trivial ring.

Equations

• IsLocalization.uniqueOfZeroMem h = uniqueOfZeroEqOne ⋯

theorem IsLocalization.mk'_eq_iff_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x₁ x₂ : R} {y₁ y₂ : ↥M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ (algebraMap R S) (↑y₂ * x₁) = (algebraMap R S) (↑y₁ * x₂)

theorem IsLocalization.mk'_eq_iff_eq' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x₁ x₂ : R} {y₁ y₂ : ↥M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ (algebraMap R S) (x₁ * ↑y₂) = (algebraMap R S) (x₂ * ↑y₁)

theorem IsLocalization.eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M} : mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ (c : ↥M), ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)

theorem IsLocalization.mk'_eq_zero_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (s : ↥M) : mk' S x s = 0 ↔ ∃ (m : ↥M), ↑m * x = 0

@[simp]

theorem IsLocalization.mk'_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : ↥M) : mk' S 0 s = 0

theorem IsLocalization.ne_zero_of_mk'_ne_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} {y : ↥M} (hxy : mk' S x y ≠ 0) : x ≠ 0

theorem IsLocalization.noZeroDivisors {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] [NoZeroDivisors R] : NoZeroDivisors S

Any localization of a commutative semiring without zero-divisors also has no zero-divisors.

theorem IsLocalization.sec_fst_ne_zero {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : S} (hx : x ≠ 0) : (sec M x).1 ≠ 0

theorem IsLocalization.eq_iff_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] [Algebra R P] [IsLocalization M P] {x y : R} : (algebraMap R S) x = (algebraMap R S) y ↔ (algebraMap R P) x = (algebraMap R P) y

theorem IsLocalization.mk'_eq_iff_mk'_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] [Algebra R P] [IsLocalization M P] {x₁ x₂ : R} {y₁ y₂ : ↥M} : mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂

theorem IsLocalization.mk'_eq_of_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M} (H : ↑a₂ * b₁ = ↑b₂ * a₁) : mk' S a₁ a₂ = mk' S b₁ b₂

theorem IsLocalization.mk'_eq_of_eq' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {a₁ b₁ : R} {a₂ b₂ : ↥M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : mk' S a₁ a₂ = mk' S b₁ b₂

theorem IsLocalization.mk'_cancel {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : R) (b c : ↥M) : mk' S (a * ↑c) (b * c) = mk' S a b

@[simp]

theorem IsLocalization.mk'_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : R} (hx : x ∈ M) : mk' S x ⟨x, hx⟩ = 1

@[simp]

theorem IsLocalization.mk'_self' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : ↥M} : mk' S (↑x) x = 1

theorem IsLocalization.mk'_self'' {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : ↥M} : mk' S (↑x) x = 1

theorem IsLocalization.mul_mk'_eq_mk'_of_mul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (z : ↥M) : (algebraMap R S) x * mk' S y z = mk' S (x * y) z

theorem IsLocalization.mk'_eq_mul_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : mk' S x y = (algebraMap R S) x * mk' S 1 y

@[simp]

theorem IsLocalization.mk'_mul_cancel_left {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : mk' S (↑y * x) y = (algebraMap R S) x

theorem IsLocalization.mk'_mul_cancel_right {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : mk' S (x * ↑y) y = (algebraMap R S) x

@[simp]

theorem IsLocalization.mk'_mul_mk'_eq_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : ↥M) : mk' S (↑x) y * mk' S (↑y) x = 1

theorem IsLocalization.mk'_mul_mk'_eq_one' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) (h : x ∈ M) : mk' S x y * mk' S ↑y ⟨x, h⟩ = 1

theorem IsLocalization.smul_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x y : R) (m : ↥M) : x • mk' S y m = mk' S (x * y) m

@[simp]

theorem IsLocalization.smul_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : R) (m : ↥M) : x • mk' S 1 m = mk' S x m

@[simp]

theorem IsLocalization.smul_mk'_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {m : ↥M} {r : R} : ↑m • mk' S r m = (algebraMap R S) r

noncomputable instance IsLocalization.invertible_mk'_one {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : ↥M) : Invertible (mk' S 1 s)

Equations

• IsLocalization.invertible_mk'_one s = { invOf := (algebraMap R S) ↑s, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem IsLocalization.invertible_mk'_one_invOf {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : ↥M) : ⅟ (mk' S 1 s) = (algebraMap R S) ↑s

theorem IsLocalization.isUnit_comp {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j : S →+* P) (y : ↥M) : IsUnit ((j.comp (algebraMap R S)) ↑y)

theorem IsLocalization.eq_of_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) {x y : R} (h : (algebraMap R S) x = (algebraMap R S) y) : g x = g y

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g(M) ⊆ Units P, f x = f y → g x = g y for all x y : R.

theorem IsLocalization.mk'_add {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : ↥M) : mk' S (x₁ * ↑y₂ + x₂ * ↑y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂

theorem IsLocalization.mul_add_inv_left {R : Type u_1} [CommSemiring R] {M : Submonoid R} {P : Type u_3} [CommSemiring P] {g : R →+* P} (h : ∀ (y : ↥M), IsUnit (g ↑y)) (y : ↥M) (w z₁ z₂ : P) : w * ↑((IsUnit.liftRight ((↑g).restrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

theorem IsLocalization.lift_spec_mul_add {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (z : S) (w w' v : P) : ((toLocalizationMap M S).lift hg) z * w + w' = v ↔ g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' = g ↑((toLocalizationMap M S).sec z).2 * v

noncomputable def IsLocalization.lift {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) : S →+* P

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g y is invertible for all y : M, the homomorphism induced from S to P sending z : S to g x * (g y)⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations

• IsLocalization.lift hg = { toFun := (↑((IsLocalization.toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem IsLocalization.lift_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) (y : ↥M) : (lift hg) (mk' S x y) = g x * ↑((IsUnit.liftRight ((↑g).restrict M) hg) y)⁻¹

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →* P such that g y is invertible for all y : M, the homomorphism induced from S to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : R, y ∈ M.

theorem IsLocalization.lift_mk'_spec {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) (v : P) (y : ↥M) : (lift hg) (mk' S x y) = v ↔ g x = g ↑y * v

@[simp]

theorem IsLocalization.lift_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) : (lift hg) ((algebraMap R S) x) = g x

theorem IsLocalization.lift_eq_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) {x y : R × ↥M} : (lift hg) (mk' S x.1 x.2) = (lift hg) (mk' S y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

@[simp]

theorem IsLocalization.lift_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) : (lift hg).comp (algebraMap R S) = g

@[simp]

theorem IsLocalization.lift_of_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j : S →+* P) : lift ⋯ = j

theorem IsLocalization.monoidHom_ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] ⦃j k : S →* P⦄ (h : j.comp ↑(algebraMap R S) = k.comp ↑(algebraMap R S)) : j = k

See note [partially-applied ext lemmas]

theorem IsLocalization.ringHom_ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] ⦃j k : S →+* P⦄ (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) : j = k

See note [partially-applied ext lemmas]

theorem IsLocalization.ext {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1) (hjm : ∀ (a b : S), j (a * b) = j a * j b) (hkm : ∀ (a b : S), k (a * b) = k a * k b) (h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)) : j = k

To show j and k agree on the whole localization, it suffices to show they agree on the image of the base ring, if they preserve 1 and *.

theorem IsLocalization.lift_unique {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) {j : S →+* P} (hj : ∀ (x : R), j ((algebraMap R S) x) = g x) : lift hg = j

@[simp]

theorem IsLocalization.lift_id {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (x : S) : (lift ⋯) x = x

theorem IsLocalization.lift_surjective_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) : Function.Surjective ⇑(lift hg) ↔ ∀ (v : P), ∃ (x : R × ↥M), v * g ↑x.2 = g x.1

theorem IsLocalization.lift_injective_iff {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (hg : ∀ (y : ↥M), IsUnit (g ↑y)) : Function.Injective ⇑(lift hg) ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ g x = g y

theorem IsLocalization.injective_iff_map_algebraMap_eq {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {T : Type u_4} [CommSemiring T] (f : S →+* T) : Function.Injective ⇑f ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

noncomputable def IsLocalization.map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (g : R →+* P) (hy : M ≤ Submonoid.comap g T) : S →+* Q

Map a homomorphism g : R →+* P to S →+* Q, where S and Q are localizations of R and P at M and T respectively, such that g(M) ⊆ T.

We send z : S to algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Equations

• IsLocalization.map Q g hy = IsLocalization.lift ⋯

@[simp]

theorem IsLocalization.map_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) (x : R) : (map Q g hy) ((algebraMap R S) x) = (algebraMap P Q) (g x)

@[simp]

theorem IsLocalization.map_comp {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) : (map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g

theorem IsLocalization.map_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) (x : R) (y : ↥M) : (map Q g hy) (mk' S x y) = mk' Q (g x) ⟨g ↑y, ⋯⟩

theorem IsLocalization.map_unique {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) (j : S →+* Q) (hj : ∀ (x : R), j ((algebraMap R S) x) = (algebraMap P Q) (g x)) : map Q g hy = j

theorem IsLocalization.map_comp_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) {A : Type u_5} [CommSemiring A] {U : Submonoid A} {W : Type u_6} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A} (hl : T ≤ Submonoid.comap l U) : (map W l hl).comp (map Q g hy) = map W (l.comp g) ⋯

If CommSemiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

theorem IsLocalization.map_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) {A : Type u_5} [CommSemiring A] {U : Submonoid A} {W : Type u_6} [CommSemiring W] [Algebra A W] [IsLocalization U W] {l : P →+* A} (hl : T ≤ Submonoid.comap l U) (x : S) : (map W l hl) ((map Q g hy) x) = (map W (l.comp g) ⋯) x

If CommSemiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

theorem IsLocalization.map_smul {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (hy : M ≤ Submonoid.comap g T) (x : S) (z : R) : (map Q g hy) (z • x) = g z • (map Q g hy) x

@[simp]

theorem IsLocalization.map_id_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {Q : Type u_5} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x : R) (y : ↥M) : (map Q (RingHom.id R) ⋯) (mk' S x y) = mk' Q x y

@[simp]

theorem IsLocalization.map_id {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (z : S) (h : M ≤ Submonoid.comap (RingHom.id R) M := ⋯) : (map S (RingHom.id R) h) z = z

noncomputable def IsLocalization.ringEquivOfRingEquiv {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) : S ≃+* Q

If S, Q are localizations of R and P at submonoids M, T respectively, an isomorphism j : R ≃+* P such that j(M) = T induces an isomorphism of localizations S ≃+* Q.

Equations

• IsLocalization.ringEquivOfRingEquiv S Q h H = { toFun := ⇑(IsLocalization.map Q ↑h ⋯), invFun := ⇑(IsLocalization.map S ↑h.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem IsLocalization.ringEquivOfRingEquiv_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : S) : (ringEquivOfRingEquiv S Q h H) a = (map Q ↑h ⋯) a

@[simp]

theorem IsLocalization.ringEquivOfRingEquiv_symm_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] (h : R ≃+* P) (H : Submonoid.map h.toMonoidHom M = T) (a : Q) : (ringEquivOfRingEquiv S Q h H).symm a = (map S ↑h.symm ⋯) a

theorem IsLocalization.ringEquivOfRingEquiv_eq_map {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) : ↑(ringEquivOfRingEquiv S Q j H) = map Q ↑j ⋯

theorem IsLocalization.ringEquivOfRingEquiv_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) : (ringEquivOfRingEquiv S Q j H) ((algebraMap R S) x) = (algebraMap P Q) (j x)

theorem IsLocalization.ringEquivOfRingEquiv_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j.toMonoidHom M = T) (x : R) (y : ↥M) : (ringEquivOfRingEquiv S Q j H) (mk' S x y) = mk' Q (j x) ⟨j ↑y, ⋯⟩

@[simp]

theorem IsLocalization.ringEquivOfRingEquiv_symm {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {T : Submonoid P} {Q : Type u_4} [CommSemiring Q] [Algebra P Q] [IsLocalization T Q] {j : R ≃+* P} (H : Submonoid.map j M = T) : (ringEquivOfRingEquiv S Q j H).symm = ringEquivOfRingEquiv Q S j.symm ⋯

theorem IsLocalization.at_units {R : Type u_1} [CommSemiring R] (S : Submonoid R) (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R

theorem IsLocalization.map_injective_of_injective {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (h : Function.Injective ⇑g) [IsLocalization (Submonoid.map g M) Q] : Function.Injective ⇑(map Q g ⋯)

Injectivity of a map descends to the map induced on localizations.

theorem IsLocalization.map_surjective_of_surjective {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] {g : R →+* P} (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (h : Function.Surjective ⇑g) [IsLocalization (Submonoid.map g M) Q] : Function.Surjective ⇑(map Q g ⋯)

Surjectivity of a map descends to the map induced on localizations.

theorem IsLocalization.isLocalization_of_base_ringEquiv {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] (h : R ≃+* P) : IsLocalization (Submonoid.map h M) S

theorem IsLocalization.isLocalization_iff_of_base_ringEquiv {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (h : R ≃+* P) : IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S

theorem IsLocalization.nonZeroDivisors_le_comap {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors S)

theorem IsLocalization.map_nonZeroDivisors_le {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S

Constructing a localization at a given submonoid

instance Localization.instUniqueLocalization {R : Type u_1} [CommSemiring R] {M : Submonoid R} [Subsingleton R] : Unique (Localization M)

Equations

• Localization.instUniqueLocalization = { toInhabited := OreLocalization.instInhabited, uniq := ⋯ }

theorem Localization.add_mk {R : Type u_1} [CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R) (d : ↥M) : mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)

theorem Localization.add_mk_self {R : Type u_1} [CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R) : mk a b + mk c b = mk (a + c) b

def Localization.mkAddMonoidHom {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : ↥M) : R →+ Localization M

For any given denominator b : M, the map a ↦ a / b is an AddMonoidHom from R to Localization M.

Equations

• Localization.mkAddMonoidHom b = { toFun := fun (a : R) => Localization.mk a b, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Localization.mkAddMonoidHom_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : ↥M) (a : R) : (mkAddMonoidHom b) a = mk a b

theorem Localization.mk_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} {ι : Type u_4} (f : ι → R) (s : Finset ι) (b : ↥M) : mk (∑ i ∈ s, f i) b = ∑ i ∈ s, mk (f i) b

theorem Localization.mk_list_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : List R) (b : ↥M) : mk l.sum b = (List.map (fun (a : R) => mk a b) l).sum

theorem Localization.mk_multiset_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : Multiset R) (b : ↥M) : mk l.sum b = (Multiset.map (fun (a : R) => mk a b) l).sum

instance Localization.isLocalization {R : Type u_1} [CommSemiring R] {M : Submonoid R} : IsLocalization M (Localization M)

instance Localization.instNoZeroDivisors {R : Type u_1} [CommSemiring R] {M : Submonoid R} [NoZeroDivisors R] : NoZeroDivisors (Localization M)

@[simp]

theorem Localization.toLocalizationMap_eq_monoidOf {R : Type u_1} [CommSemiring R] {M : Submonoid R} : IsLocalization.toLocalizationMap M (Localization M) = monoidOf M

theorem Localization.monoidOf_eq_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) : (monoidOf M).toMap x = (algebraMap R (Localization M)) x

theorem Localization.mk_one_eq_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) : mk x 1 = (algebraMap R (Localization M)) x

theorem Localization.mk_eq_mk'_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) (y : ↥M) : mk x y = IsLocalization.mk' (Localization M) x y

theorem Localization.mk_eq_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} : mk = IsLocalization.mk' (Localization M)

theorem Localization.mk_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} {A : Type u_4} [CommSemiring A] [Algebra A R] (m : A) : mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

theorem Localization.neg_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a : R) (b : ↥M) : -mk a b = mk (-a) b

theorem Localization.sub_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a c : R) (b d : ↥M) : mk a b - mk c d = mk (↑d * a - ↑b * c) (b * d)

theorem IsLocalization.mk'_neg {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (x : R) (y : ↥M) : mk' S (-x) y = -mk' S x y

theorem IsLocalization.mk'_sub {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : ↥M) : mk' S (x₁ * ↑y₂ - x₂ * ↑y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

theorem IsLocalization.injective_of_map_algebraMap_zero {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {T : Type u_5} [CommRing T] (f : S →+* T) (h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0) : Function.Injective ⇑f

theorem IsLocalization.to_map_eq_zero_iff {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] {x : R} (hM : M ≤ nonZeroDivisors R) : (algebraMap R S) x = 0 ↔ x = 0

theorem IsLocalization.injective {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (hM : M ≤ nonZeroDivisors R) : Function.Injective ⇑(algebraMap R S)

theorem IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] [Nontrivial R] (hM : M ≤ nonZeroDivisors R) {x : R} (hx : x ∈ nonZeroDivisors R) : (algebraMap R S) x ≠ 0

theorem IsLocalization.sec_snd_ne_zero {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] [Nontrivial R] (hM : M ≤ nonZeroDivisors R) (x : S) : ↑(sec M x).2 ≠ 0

@[deprecated IsLocalization.noZeroDivisors (since := "2025-03-18")]

theorem IsLocalization.noZeroDivisors_of_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] [NoZeroDivisors R] : NoZeroDivisors S

Alias of IsLocalization.noZeroDivisors.

---

Any localization of a commutative semiring without zero-divisors also has no zero-divisors.

theorem IsLocalization.isDomain_of_le_nonZeroDivisors {S : Type u_2} [CommRing S] (A : Type u_6) [CommRing A] [IsDomain A] [Algebra A S] {M : Submonoid A} [IsLocalization M S] (hM : M ≤ nonZeroDivisors A) : IsDomain S

A CommRing S which is the localization of an integral domain R at a subset of non-zero elements is an integral domain.

theorem IsLocalization.isDomain_localization {A : Type u_6} [CommRing A] [IsDomain A] {M : Submonoid A} (hM : M ≤ nonZeroDivisors A) : IsDomain (Localization M)

The localization of an integral domain to a set of non-zero elements is an integral domain.