Documentation

Mathlib.RingTheory.Localization.Basic

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

    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.
    Instances For
      @[inline, reducible]

      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 { val := y, property := 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 { val := y, property := 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'_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.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} :
                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 { val := x, property := 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 { val := x, property := 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 ((RingHom.comp j (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 (MonoidHom.restrict (g) M) h) y)⁻¹ + z₁ = z₂ w + g y * z₁ = g y * z₂
                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.
                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) :

                  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)) :
                  @[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 : MonoidHom.comp j (algebraMap R S) = MonoidHom.comp k (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 : RingHom.comp j (algebraMap R S) = RingHom.comp k (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
                  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] (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] :
                    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) { val := g y, property := }
                    @[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) ) :
                    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)) :
                    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) :

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

                    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]
                    @[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 (RingEquiv.toMonoidHom h) M = T) (a : S) :
                    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 (RingEquiv.toMonoidHom h) 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.
                    Instances For
                      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 (RingEquiv.toMonoidHom j) 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 (RingEquiv.toMonoidHom j) M = T) (x : R) (y : M) :
                      (IsLocalization.ringEquivOfRingEquiv S Q j H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (j x) { val := j y, property := }
                      @[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) :
                      @[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) :
                      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] :

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

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

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

                        Equations
                        Instances For
                          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.

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

                          Constructing a localization at a given submonoid #

                          Equations
                          theorem Localization.add_def {R : Type u_4} [CommSemiring R] {M : Submonoid R} (z : Localization M) (w : Localization M) :
                          Localization.add z w = Localization.liftOn₂ z w (fun (a : R) (b : M) (c : R) (d : M) => Localization.mk (b * c + d * a) (b * d))
                          @[irreducible]

                          Addition in a ring localization is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨b * c + d * a, b * d⟩.

                          Should not be confused with AddLocalization.add, which is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩.

                          Equations
                          Instances For
                            Equations
                            • Localization.instAddLocalizationToCommMonoid = { add := Localization.add }
                            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) :
                            Equations
                            • Localization.instCommSemiringLocalizationToCommMonoid = let __src := let_fun this := inferInstance; this; CommSemiring.mk
                            @[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 (Finset.sum s fun (i : ι) => f i) b = Finset.sum s fun (i : ι) => Localization.mk (f i) b
                              theorem Localization.mk_list_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : List R) (b : M) :
                              theorem Localization.mk_multiset_sum {R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : Multiset R) (b : M) :
                              instance Localization.algebra {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_4} [CommSemiring S] [Algebra S R] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              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.mk_nat_cast {R : Type u_1} [CommSemiring R] {M : Submonoid R} (m : ) :
                              Localization.mk (m) 1 = m
                              @[simp]
                              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] :

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

                              Equations
                              Instances For
                                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
                                Instances For
                                  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) :
                                  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) :
                                  @[irreducible]
                                  def Localization.neg {R : Type u_4} [CommRing R] {M : Submonoid R} (z : Localization M) :

                                  Negation in a ring localization is defined as -⟨a, b⟩ = ⟨-a, b⟩.

                                  Equations
                                  Instances For
                                    theorem Localization.neg_def {R : Type u_4} [CommRing R] {M : Submonoid R} (z : Localization M) :
                                    Localization.neg z = Localization.liftOn z (fun (a : R) (b : M) => Localization.mk (-a) b)
                                    Equations
                                    • Localization.instNegLocalizationToCommMonoid = { neg := Localization.neg }
                                    theorem Localization.neg_mk {R : Type u_1} [CommRing R] {M : Submonoid R} (a : R) (b : M) :
                                    Equations
                                    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_int_cast {R : Type u_1} [CommRing R] {M : Submonoid R} (m : ) :
                                    Localization.mk (m) 1 = m
                                    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) :
                                    @[reducible]

                                    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. See note [reducible non-instances].

                                    @[reducible]

                                    A CommRing S which is the localization of an integral domain R at a subset of non-zero elements is an integral domain. See note [reducible non-instances].

                                    @[reducible]

                                    The localization of an integral domain to a set of non-zero elements is an integral domain. See note [reducible non-instances].

                                    theorem IsField.localization_map_bijective {R : Type u_4} {Rₘ : Type u_5} [CommRing R] [CommRing Rₘ] {M : Submonoid R} (hM : 0M) (hR : IsField R) [Algebra R Rₘ] [IsLocalization M 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 : 0M) [Algebra K Kₘ] [IsLocalization M 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
                                    Instances For
                                      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ₘ] [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra R Sₘ] [IsScalarTower R S 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) { val := (algebraMap R S) y, property := }
                                      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ₘ] :
                                      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)) :

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