Documentation

Mathlib.RingTheory.Localization.Defs

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 #

Main results #

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] :

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.

Instances
    theorem IsLocalization.map_units' {R : Type u_1} :
    ∀ {inst : CommSemiring R} {M : Submonoid R} {S : Type u_2} {inst_1 : CommSemiring S} {inst_2 : 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} :
    ∀ {inst : CommSemiring R} {M : Submonoid R} {S : Type u_2} {inst_1 : CommSemiring S} {inst_2 : 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} :
    ∀ {inst : CommSemiring R} {M : Submonoid R} {S : Type u_2} {inst_1 : CommSemiring S} {inst_2 : Algebra R S} [self : 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.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₂ : rN, IsUnit ((algebraMap R S) r)) :
    @[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
    Instances For
      @[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
      Instances For
        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
        Instances For
          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) :

          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) :

          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) :

          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
          Instances For
            @[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) :
            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) :
            @[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.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) :
            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] :

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

            Equations
            Instances For
              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) :

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

              Equations
              Instances For
                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.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) :
                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) :
                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) :
                @[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) :
                @[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) :
                @[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) :
                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) :
                Equations
                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
                Instances For
                  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) :
                  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.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 : SP) (k : SP) (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) :
                  @[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) :
                  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
                  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} [CommRing 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
                  Instances For
                    @[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) :
                    (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] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) :
                    (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] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (x : R) (y : M) :
                    (IsLocalization.map Q g hy) (IsLocalization.mk' S x y) = IsLocalization.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)) :
                    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) :
                    (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] [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) :
                    (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] [Algebra P Q] [IsLocalization T Q] (hy : M Submonoid.comap g T) (x : S) (z : R) :
                    (IsLocalization.map Q g hy) (z x) = g z (IsLocalization.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) :
                    @[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) ) :
                    @[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) :
                    @[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
                    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
                    Instances For
                      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) :
                      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) :
                      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) :
                      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] :

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

                      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.toMonoidHom M) S

                      Constructing a localization at a given submonoid #

                      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) :
                      @[simp]
                      def Localization.mkAddMonoidHom {R : Type u_1} [CommSemiring R] {M : Submonoid R} (b : M) :

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

                      Equations
                      Instances For
                        theorem Localization.mk_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} {ι : Type u_4} (f : ιR) (s : Finset ι) (b : M) :
                        Localization.mk (∑ is, f i) b = is, 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
                        Equations
                        • =
                        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) :
                        theorem Localization.neg_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a : R) (b : M) :
                        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 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) :
                        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) :
                        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) :

                        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.

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

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