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
• IsLocalization.algEquiv: if Q is another localization of R at M, then S and Q are isomorphic as R-algebras

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

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

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.map_units' {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [self : 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] [self : 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.exists_of_eq {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [self : IsLocalization M S] {x : R} {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.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 : R} {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.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

@[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) : (↑(IsLocalization.toLocalizationWithZeroMap M S).toMonoidHom).toFun a = (algebraMap R S) a

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

• One or more equations did not get rendered due to their size.

@[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] : (IsLocalization.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) : (IsLocalization.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 : S) (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] : (IsLocalization.toLocalizationMap M S).sec = IsLocalization.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) ↑(IsLocalization.sec M z).2 = (algebraMap R S) (IsLocalization.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) (IsLocalization.sec M z).1 = (algebraMap R S) ↑(IsLocalization.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.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 : R} {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 : R} {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) : IsLocalization.mk' S (IsLocalization.sec M z).1 (IsLocalization.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₁ : R) (x₂ : R) (y₁ : ↥M) (y₂ : ↥M) : IsLocalization.mk' S (x₁ * x₂) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ * IsLocalization.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) : IsLocalization.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) : IsLocalization.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 * IsLocalization.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 : R) (y : R) (hy : y ∈ M) : IsLocalization.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 : R) (y : R) (hy : y ∈ M) : (algebraMap R S) y * IsLocalization.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 = IsLocalization.mk' S x y ↔ z * (algebraMap R S) ↑y = (algebraMap R S) x

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} : IsLocalization.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₁ : S} {z₂ : S} : IsLocalization.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 : ℕ) : IsLocalization.mk' S (x ^ n) (y ^ n) = IsLocalization.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), IsLocalization.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 = let_fun this := Classical.propDecidable; 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₁ : R} {x₂ : R} {y₁ : ↥M} {y₂ : ↥M} : IsLocalization.mk' S x₁ y₁ = IsLocalization.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₁ : R} {x₂ : R} {y₁ : ↥M} {y₂ : ↥M} : IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ (algebraMap R S) (x₁ * ↑y₂) = (algebraMap R S) (x₂ * ↑y₁)

theorem IsLocalization.mk'_mem_iff {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} {I : Ideal S} : IsLocalization.mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I

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₁ : R} {b₁ : R} {a₂ : ↥M} {b₂ : ↥M} : IsLocalization.mk' S a₁ a₂ = IsLocalization.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) : IsLocalization.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) : IsLocalization.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 : IsLocalization.mk' S x y ≠ 0) : x ≠ 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 : R} {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₁ : R} {x₂ : R} {y₁ : ↥M} {y₂ : ↥M} : IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ IsLocalization.mk' P x₁ y₁ = IsLocalization.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₁ : R} {b₁ : R} {a₂ : ↥M} {b₂ : ↥M} (H : ↑a₂ * b₁ = ↑b₂ * a₁) : IsLocalization.mk' S a₁ a₂ = IsLocalization.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₁ : R} {b₁ : R} {a₂ : ↥M} {b₂ : ↥M} (H : b₁ * ↑a₂ = a₁ * ↑b₂) : IsLocalization.mk' S a₁ a₂ = IsLocalization.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 : ↥M) (c : ↥M) : IsLocalization.mk' S (a * ↑c) (b * c) = IsLocalization.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) : IsLocalization.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} : IsLocalization.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} : IsLocalization.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 : R) (y : R) (z : ↥M) : (algebraMap R S) x * IsLocalization.mk' S y z = IsLocalization.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) : IsLocalization.mk' S x y = (algebraMap R S) x * IsLocalization.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) : IsLocalization.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) : IsLocalization.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 : ↥M) (y : ↥M) : IsLocalization.mk' S (↑x) y * IsLocalization.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) : IsLocalization.mk' S x y * IsLocalization.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 : R) (y : R) (m : ↥M) : x • IsLocalization.mk' S y m = IsLocalization.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 • IsLocalization.mk' S 1 m = IsLocalization.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 • IsLocalization.mk' S r m = (algebraMap R S) r

@[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) : ⅟(IsLocalization.mk' S 1 s) = (algebraMap R S) ↑s

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 (IsLocalization.mk' S 1 s)

Equations

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

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 : R} {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₁ : R) (x₂ : R) (y₁ : ↥M) (y₂ : ↥M) : IsLocalization.mk' S (x₁ * ↑y₂ + x₂ * ↑y₁) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ + IsLocalization.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 : P) (z₁ : P) (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 : P) (w' : P) (v : P) : ((IsLocalization.toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg) z * w + w' = v ↔ g ((IsLocalization.toLocalizationMap M S).sec z).1 * w + g ↑((IsLocalization.toLocalizationMap M S).sec z).2 * w' = g ↑((IsLocalization.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

• One or more equations did not get rendered due to their size.

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) : (IsLocalization.lift hg) (IsLocalization.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) : (IsLocalization.lift hg) (IsLocalization.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) : (IsLocalization.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 : R × ↥M} {y : R × ↥M} : (IsLocalization.lift hg) (IsLocalization.mk' S x.1 x.2) = (IsLocalization.lift hg) (IsLocalization.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)) : (IsLocalization.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) : IsLocalization.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 : S →* P⦄ ⦃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 : S →+* P⦄ ⦃k : S →+* P⦄ (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) : j = k

See note [partially-applied ext lemmas]

theorem IsLocalization.algHom_subsingleton {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] : Subsingleton (S →ₐ[R] P)

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 : S → P) (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) : IsLocalization.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) : (IsLocalization.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 ⇑(IsLocalization.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 ⇑(IsLocalization.lift hg) ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ g x = g 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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] (x : R) : (IsLocalization.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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] : (IsLocalization.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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] (x : R) (y : ↥M) : (IsLocalization.map Q g hy) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (g x) ⟨g ↑y, ⋯⟩

@[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) : (IsLocalization.map Q (RingHom.id R) ⋯) (IsLocalization.mk' S x y) = IsLocalization.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 : optParam (M ≤ Submonoid.comap (RingHom.id R) M) ⋯) : (IsLocalization.map S (RingHom.id R) h) z = z

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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] (j : S →+* Q) (hj : ∀ (x : R), j ((algebraMap R S) x) = (algebraMap P Q) (g x)) : IsLocalization.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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] {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) : (IsLocalization.map W l hl).comp (IsLocalization.map Q g hy) = IsLocalization.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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] {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) : (IsLocalization.map W l hl) ((IsLocalization.map Q g hy) x) = (IsLocalization.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] (hy : M ≤ Submonoid.comap g T) [Algebra P Q] [IsLocalization T Q] (x : S) (z : R) : (IsLocalization.map Q g hy) (z • x) = g z • (IsLocalization.map Q g hy) x

@[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) : (IsLocalization.ringEquivOfRingEquiv S Q h H).symm a = (IsLocalization.map S ↑h.symm ⋯) a

@[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) : (IsLocalization.ringEquivOfRingEquiv S Q h H) a = (IsLocalization.map Q ↑h ⋯) a

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

• One or more equations did not get rendered due to their size.

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) : ↑(IsLocalization.ringEquivOfRingEquiv S Q j H) = IsLocalization.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) : (IsLocalization.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) : (IsLocalization.ringEquivOfRingEquiv S Q j H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (j x) ⟨j ↑y, ⋯⟩

@[simp]

theorem IsLocalization.algEquiv_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (Q : Type u_4) [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (a : S) : (IsLocalization.algEquiv M S Q) a = (IsLocalization.map Q (RingHom.id R) ⋯) a

@[simp]

theorem IsLocalization.algEquiv_symm_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (Q : Type u_4) [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (a : Q) : (IsLocalization.algEquiv M S Q).symm a = (IsLocalization.map S (RingHom.id R) ⋯) a

noncomputable def IsLocalization.algEquiv {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (Q : Type u_4) [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] : S ≃ₐ[R] Q

If S, Q are localizations of R at the submonoid M respectively, there is an isomorphism of localizations S ≃ₐ[R] Q.

Equations

• IsLocalization.algEquiv M S Q = let __src := IsLocalization.ringEquivOfRingEquiv S Q (RingEquiv.refl R) ⋯; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem IsLocalization.algEquiv_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_4} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x : R) (y : ↥M) : (IsLocalization.algEquiv M S Q) (IsLocalization.mk' S x y) = IsLocalization.mk' Q x y

theorem IsLocalization.algEquiv_symm_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_4} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (x : R) (y : ↥M) : (IsLocalization.algEquiv M S Q).symm (IsLocalization.mk' Q x y) = IsLocalization.mk' S x y

theorem IsLocalization.bijective {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {Q : Type u_4} [CommSemiring Q] [Algebra R Q] [IsLocalization M Q] (f : S →+* Q) (hf : f.comp (algebraMap R S) = algebraMap R Q) : Function.Bijective ⇑f

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

noncomputable def IsLocalization.atUnits (R : Type u_1) [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (H : M ≤ IsUnit.submonoid R) : R ≃ₐ[R] S

The localization at a module of units is isomorphic to the ring.

Equations

• IsLocalization.atUnits R M H = AlgEquiv.ofBijective (Algebra.ofId R S) ⋯

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 ⇑(IsLocalization.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 ⇑(IsLocalization.map Q g ⋯)

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

theorem IsLocalization.isLocalization_of_algEquiv {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) : IsLocalization M P

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

theorem IsLocalization.isLocalization_iff_of_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 : S ≃+* P) : IsLocalization M S ↔ IsLocalization M P

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.toMonoidHom 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.toMonoidHom 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) : Localization.mk a b + Localization.mk c d = Localization.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) : Localization.mk a b + Localization.mk c b = Localization.mk (a + c) b

@[simp]

theorem Localization.mkAddMonoidHom_apply {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : ↥M) (a : R) : (Localization.mkAddMonoidHom b) a = Localization.mk a 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' := ⋯ }

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

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

theorem Localization.monoidOf_eq_algebraMap {R : Type u_1} [CommSemiring R] {M : Submonoid R} (x : R) : (Localization.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) : Localization.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) : Localization.mk x y = IsLocalization.mk' (Localization M) x y

theorem Localization.mk_eq_mk' {R : Type u_1} [CommSemiring R] {M : Submonoid R} : Localization.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) : Localization.mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

theorem Localization.mk_natCast {R : Type u_1} [CommSemiring R] {M : Submonoid R} (m : ℕ) : Localization.mk (↑m) 1 = ↑m

@[deprecated Localization.mk_natCast]

theorem Localization.mk_nat_cast {R : Type u_1} [CommSemiring R] {M : Submonoid R} (m : ℕ) : Localization.mk (↑m) 1 = ↑m

Alias of Localization.mk_natCast.

@[simp]

theorem Localization.algEquiv_symm_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : S) : (Localization.algEquiv M S).symm a = (IsLocalization.map (Localization M) (RingHom.id R) ⋯) a

@[simp]

theorem Localization.algEquiv_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : Localization M) : (Localization.algEquiv M S) a = (IsLocalization.map S (RingHom.id R) ⋯) a

noncomputable def Localization.algEquiv {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : Localization M ≃ₐ[R] S

The localization of R at M as a quotient type is isomorphic to any other localization.

Equations

• Localization.algEquiv M S = IsLocalization.algEquiv M (Localization M) S

noncomputable def IsLocalization.unique (R : Type u_4) (Rₘ : Type u_5) [CommSemiring R] [CommSemiring Rₘ] (M : Submonoid R) [Subsingleton R] [Algebra R Rₘ] [IsLocalization M Rₘ] : Unique Rₘ

The localization of a singleton is a singleton. Cannot be an instance due to metavariables.

Equations

• IsLocalization.unique R Rₘ M = let_fun this := { default := 1 }; ⋯.unique

theorem Localization.algEquiv_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) : (Localization.algEquiv M S) (IsLocalization.mk' (Localization M) x y) = IsLocalization.mk' S x y

theorem Localization.algEquiv_symm_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) : (Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = IsLocalization.mk' (Localization M) x y

theorem Localization.algEquiv_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) : (Localization.algEquiv M S) (Localization.mk x y) = IsLocalization.mk' S x y

theorem Localization.algEquiv_symm_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) : (Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = Localization.mk x y

theorem Localization.coe_algEquiv {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : ↑(Localization.algEquiv M S) = IsLocalization.map S (RingHom.id R) ⋯

theorem Localization.coe_algEquiv_symm {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] : ↑(Localization.algEquiv M S).symm = IsLocalization.map (Localization M) (RingHom.id R) ⋯

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

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

theorem Localization.mk_intCast {R : Type u_1} [CommRing R] {M : Submonoid R} (m : ℤ) : Localization.mk (↑m) 1 = ↑m

@[deprecated Localization.mk_intCast]

theorem Localization.mk_int_cast {R : Type u_1} [CommRing R] {M : Submonoid R} (m : ℤ) : Localization.mk (↑m) 1 = ↑m

Alias of Localization.mk_intCast.

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) : ↑(IsLocalization.sec M x).2 ≠ 0

theorem IsLocalization.sec_fst_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] [NoZeroDivisors S] (hM : M ≤ nonZeroDivisors R) {x : S} (hx : x ≠ 0) : (IsLocalization.sec M x).1 ≠ 0

theorem IsLocalization.noZeroDivisors_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) : NoZeroDivisors S

A CommRing S which is the localization of a ring R without zero divisors at a subset of non-zero elements does not have 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.

theorem IsField.localization_map_bijective {R : Type u_4} {Rₘ : Type u_5} [CommRing R] [CommRing Rₘ] {M : Submonoid R} (hM : 0 ∉ M) (hR : IsField R) [Algebra R Rₘ] [IsLocalization M Rₘ] : Function.Bijective ⇑(algebraMap R Rₘ)

If R is a field, then localizing at a submonoid not containing 0 adds no new elements.

theorem Field.localization_map_bijective {K : Type u_4} {Kₘ : Type u_5} [Field K] [CommRing Kₘ] {M : Submonoid K} (hM : 0 ∉ M) [Algebra K Kₘ] [IsLocalization M Kₘ] : Function.Bijective ⇑(algebraMap K Kₘ)

If R is a field, then localizing at a submonoid not containing 0 adds no new elements.

noncomputable def localizationAlgebra {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] : Algebra Rₘ Sₘ

Definition of the natural algebra induced by the localization of an algebra. Given an algebra R → S, a submonoid R of M, and a localization Rₘ for M, let Sₘ be the localization of S to the image of M under algebraMap R S. Then this is the natural algebra structure on Rₘ → Sₘ, such that the entire square commutes, where localization_map.map_comp gives the commutativity of the underlying maps.

This instance can be helpful if you define Sₘ := Localization (Algebra.algebraMapSubmonoid S M), however we will instead use the hypotheses [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] in lemmas since the algebra structure may arise in different ways.

Equations

• localizationAlgebra M S = (IsLocalization.map Sₘ (algebraMap R S) ⋯).toAlgebra

theorem IsLocalization.map_units_map_submonoid {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [Algebra R Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] (y : ↥M) : IsUnit ((algebraMap R Sₘ) ↑y)

theorem IsLocalization.algebraMap_mk' {R : Type u_1} [CommRing R] {M : Submonoid R} (S : Type u_2) [CommRing S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : R) (y : ↥M) : (algebraMap Rₘ Sₘ) (IsLocalization.mk' Rₘ x y) = IsLocalization.mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩

theorem IsLocalization.algebraMap_eq_map_map_submonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] : algebraMap Rₘ Sₘ = IsLocalization.map Sₘ (algebraMap R S) ⋯

If the square below commutes, the bottom map is uniquely specified:

R  →  S
↓     ↓
Rₘ → Sₘ

theorem IsLocalization.algebraMap_apply_eq_map_map_submonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : Rₘ) : (algebraMap Rₘ Sₘ) x = (IsLocalization.map Sₘ (algebraMap R S) ⋯) x

If the square below commutes, the bottom map is uniquely specified:

R  →  S
↓     ↓
Rₘ → Sₘ

theorem IsLocalization.lift_algebraMap_eq_algebraMap {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] : IsLocalization.lift ⋯ = algebraMap Rₘ Sₘ

theorem localizationAlgebra_injective {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] (hRS : Function.Injective ⇑(algebraMap R S)) : Function.Injective ⇑(algebraMap Rₘ Sₘ)

Injectivity of the underlying algebraMap descends to the algebra induced by localization.