Localizations of commutative rings

This file contains various basic results on localizations.

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

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

@[reducible, inline]

noncomputable abbrev Localization.mapPiEvalRingHom {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → CommSemiring (R i)] {i : ι} (S : Submonoid (R i)) : Localization (Submonoid.comap (Pi.evalRingHom R i) S) →+* Localization S

IsLocalization.map applied to a projection homomorphism from a product ring.

Equations

• Localization.mapPiEvalRingHom S = IsLocalization.map (Localization S) (Pi.evalRingHom R i) ⋯

theorem Localization.mapPiEvalRingHom_bijective {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → CommSemiring (R i)] {i : ι} (S : Submonoid (R i)) : Function.Bijective ⇑(Localization.mapPiEvalRingHom S)

theorem IsLocalization.linearMap_compatibleSMul {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (N₁ : Type u_4) (N₂ : Type u_5) [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module S N₁] [Module R N₂] [Module S N₂] [IsScalarTower R S N₁] [IsScalarTower R S N₂] : LinearMap.CompatibleSMul N₁ N₂ S R

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)

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 = { toEquiv := (IsLocalization.ringEquivOfRingEquiv S Q (RingEquiv.refl R) ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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

@[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

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

noncomputable def IsLocalization.liftAlgHom {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] {P : Type u_7} [CommSemiring P] [Algebra A P] [IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)) : S →ₐ[A] P

AlgHom version of IsLocalization.lift.

Equations

• IsLocalization.liftAlgHom hf = { toRingHom := IsLocalization.lift hf, commutes' := ⋯ }

theorem IsLocalization.liftAlgHom_toRingHom {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] {P : Type u_7} [CommSemiring P] [Algebra A P] [IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)) : (IsLocalization.liftAlgHom hf).toRingHom = IsLocalization.lift hf

@[simp]

theorem IsLocalization.coe_liftAlgHom {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] {P : Type u_7} [CommSemiring P] [Algebra A P] [IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)) : ⇑(IsLocalization.liftAlgHom hf) = ⇑(IsLocalization.lift hf)

theorem IsLocalization.liftAlgHom_apply {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] {P : Type u_7} [CommSemiring P] [Algebra A P] [IsLocalization M S] {f : R →ₐ[A] P} (hf : ∀ (y : ↥M), IsUnit (f ↑y)) (x : S) : (IsLocalization.liftAlgHom hf) x = (IsLocalization.lift hf) x

noncomputable def IsLocalization.algEquivOfAlgEquiv {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} (S : Type u_6) [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} (Q : Type u_8) [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] (h : R ≃ₐ[A] P) (H : Submonoid.map h M = T) : S ≃ₐ[A] Q

If S, Q are localizations of R and P at submonoids M, T respectively, an isomorphism h : R ≃ₐ[A] P such that h(M) = T induces an isomorphism of localizations S ≃ₐ[A] Q.

Equations

• IsLocalization.algEquivOfAlgEquiv S Q h H = { toEquiv := (IsLocalization.ringEquivOfRingEquiv S Q h.toRingEquiv H).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem IsLocalization.algEquivOfAlgEquiv_apply {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} (S : Type u_6) [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} (Q : Type u_8) [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] (h : R ≃ₐ[A] P) (H : Submonoid.map h M = T) (a : S) : (IsLocalization.algEquivOfAlgEquiv S Q h H) a = (IsLocalization.map Q ↑h ⋯) a

@[simp]

theorem IsLocalization.algEquivOfAlgEquiv_symm_apply {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} (S : Type u_6) [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} (Q : Type u_8) [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] (h : R ≃ₐ[A] P) (H : Submonoid.map h M = T) (a : Q) : (IsLocalization.algEquivOfAlgEquiv S Q h H).symm a = (IsLocalization.map S ↑(↑h).symm ⋯) a

theorem IsLocalization.algEquivOfAlgEquiv_eq_map {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} {Q : Type u_8} [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] {h : R ≃ₐ[A] P} (H : Submonoid.map h M = T) : ↑(IsLocalization.algEquivOfAlgEquiv S Q h H) = IsLocalization.map Q ↑h ⋯

theorem IsLocalization.algEquivOfAlgEquiv_eq {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} {Q : Type u_8} [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] {h : R ≃ₐ[A] P} (H : Submonoid.map h M = T) (x : R) : (IsLocalization.algEquivOfAlgEquiv S Q h H) ((algebraMap R S) x) = (algebraMap P Q) (h x)

theorem IsLocalization.algEquivOfAlgEquiv_mk' {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} {Q : Type u_8} [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] {h : R ≃ₐ[A] P} (H : Submonoid.map h M = T) (x : R) (y : ↥M) : (IsLocalization.algEquivOfAlgEquiv S Q h H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (h x) ⟨h ↑y, ⋯⟩

theorem IsLocalization.algEquivOfAlgEquiv_symm {A : Type u_4} [CommSemiring A] {R : Type u_5} [CommSemiring R] [Algebra A R] {M : Submonoid R} {S : Type u_6} [CommSemiring S] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [IsLocalization M S] {P : Type u_7} [CommSemiring P] [Algebra A P] {T : Submonoid P} {Q : Type u_8} [CommSemiring Q] [Algebra A Q] [Algebra P Q] [IsScalarTower A P Q] [IsLocalization T Q] {h : R ≃ₐ[A] P} (H : Submonoid.map h M = T) : (IsLocalization.algEquivOfAlgEquiv S Q h H).symm = IsLocalization.algEquivOfAlgEquiv Q S h.symm ⋯

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.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_iff_of_isLocalization {R : Type u_1} [CommSemiring R] (M N : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] [IsLocalization M S] [IsLocalization N S] [Algebra R P] : IsLocalization M P ↔ IsLocalization N P

If an algebra is simultaneously localizations for two submonoids, then an arbitrary algebra is a localization of one submonoid iff it is a localization of the other.

theorem IsLocalization.commutes {R : Type u_1} [CommSemiring R] (S₁ : Type u_4) (S₂ : Type u_5) (T : Type u_6) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring T] [Algebra R S₁] [Algebra R S₂] [Algebra R T] [Algebra S₁ T] [Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T] (M₁ M₂ : Submonoid R) [IsLocalization M₁ S₁] [IsLocalization M₂ S₂] [IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T] : IsLocalization (Algebra.algebraMapSubmonoid S₁ M₂) T

If S₁ is the localization of R at M₁ and S₂ is the localization of R at M₂, then every localization T of S₂ at M₁ is also a localization of S₁ at M₂, in other words M₁⁻¹M₂⁻¹R can be identified with M₂⁻¹M₁⁻¹R.

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.

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

@[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

@[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

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 = ⋯.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.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 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ₘ] [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) ⟨(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.