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 ⇑(mapPiEvalRingHom S)

theorem IsLocalization.finite (R : Type u_1) [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] [Finite R] : Finite 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) : (algEquiv M S Q).symm a = (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) : (algEquiv M S Q) a = (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) : (algEquiv M S Q) (mk' S x y) = 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) : (algEquiv M S Q).symm (mk' Q x y) = 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)) : (liftAlgHom hf).toRingHom = 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)) : ⇑(liftAlgHom hf) = ⇑(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) : (liftAlgHom hf) x = (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) : (algEquivOfAlgEquiv S Q h H) a = (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) : (algEquivOfAlgEquiv S Q h H).symm a = (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) : ↑(algEquivOfAlgEquiv S Q h H) = 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) : (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) : (algEquivOfAlgEquiv S Q h H) (mk' S x y) = 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) : (algEquivOfAlgEquiv S Q h H).symm = algEquivOfAlgEquiv Q S h.symm ⋯

theorem IsLocalization.smul_mem_iff {R : Type u_4} [CommSemiring R] {S : Submonoid R} {R' : Type u_5} [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] {M' : Type u_6} [AddCommMonoid M'] [Module R' M'] [Module R M'] [IsScalarTower R R' M'] {N' : Submodule R' M'} {x : M'} {s : ↥S} : s • x ∈ N' ↔ x ∈ N'

If x in a R' = S⁻¹ R-module M', then for a submodule N' of M', s • x ∈ N' if and only if x ∈ N' for some s in S.

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.iff_of_le_of_exists_dvd {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) : IsLocalization M S ↔ IsLocalization N S

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 IsLocalization.algEquiv_comp_algebraMap {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [CommSemiring Rₘ] [CommSemiring Sₙ] [CommSemiring Rₘ'] [CommSemiring Sₙ'] [Algebra R Rₘ] [Algebra S Sₙ] [Algebra R Rₘ'] [Algebra S Sₙ'] [Algebra R Sₙ] [Algebra Rₘ Sₙ] [Algebra Rₘ' Sₙ'] [Algebra R Sₙ'] (N : Submonoid S) [IsLocalization M Rₘ] [IsLocalization N Sₙ] [IsLocalization M Rₘ'] [IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ'] [IsScalarTower R S Sₙ'] : (↑(algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ) = (algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')

theorem IsLocalization.algEquiv_comp_algebraMap_apply {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] {Rₘ : Type u_4} (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [CommSemiring Rₘ] [CommSemiring Sₙ] [CommSemiring Rₘ'] [CommSemiring Sₙ'] [Algebra R Rₘ] [Algebra S Sₙ] [Algebra R Rₘ'] [Algebra S Sₙ'] [Algebra R Sₙ] [Algebra Rₘ Sₙ] [Algebra Rₘ' Sₙ'] [Algebra R Sₙ'] (N : Submonoid S) [IsLocalization M Rₘ] [IsLocalization N Sₙ] [IsLocalization M Rₘ'] [IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ'] [IsScalarTower R S Sₙ'] (x : Rₘ) : ((↑(algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ)) x = ((algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')) x

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

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) : (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) : (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) : (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) : (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) : (algEquiv M S) (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) : (algEquiv M S).symm (IsLocalization.mk' S x y) = 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] : ↑(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] : ↑(algEquiv M S).symm = IsLocalization.map (Localization M) (RingHom.id R) ⋯

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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [CommSemiring Rₘ] [CommSemiring 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

noncomputable instance instAlgebraLocalizationAlgebraMapSubmonoid {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] : Algebra (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))

Equations

• instAlgebraLocalizationAlgebraMapSubmonoid M S = localizationAlgebra M S

instance instIsScalarTowerLocalizationAlgebraMapSubmonoid {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] : IsScalarTower R (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))

theorem IsLocalization.map_units_map_submonoid {R : Type u_1} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] (Sₘ : Type u_5) [CommSemiring 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} [CommSemiring R] {M : Submonoid R} (S : Type u_2) [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommSemiring Rₘ] [CommSemiring 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ₘ) (mk' Rₘ x y) = mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩

theorem IsLocalization.algebraMap_eq_map_map_submonoid {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommSemiring Rₘ] [CommSemiring 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ₘ = 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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommSemiring Rₘ] [CommSemiring 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 = (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} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommSemiring Rₘ] [CommSemiring 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ₘ] : lift ⋯ = algebraMap Rₘ Sₘ

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

theorem localizationAlgebra_injective {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommSemiring Rₘ] [CommSemiring 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.

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

theorem IsLocalization.algHom_ext {R : Type u_1} {A : Type u_2} {L : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring L] [Semiring B] (W : Submonoid A) [Algebra A L] [IsLocalization W L] [Algebra R A] [Algebra R L] [IsScalarTower R A L] [Algebra R B] {f g : L →ₐ[R] B} (h : f.comp (Algebra.algHom R A L) = g.comp (Algebra.algHom R A L)) : f = g

theorem Localization.algHom_ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] (W : Submonoid A) {f g : Localization W →ₐ[R] B} (h : f.comp (Algebra.algHom R A (Localization W)) = g.comp (Algebra.algHom R A (Localization W))) : f = g

theorem Localization.algHom_ext_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] {W : Submonoid A} {f g : Localization W →ₐ[R] B} : f = g ↔ f.comp (Algebra.algHom R A (Localization W)) = g.comp (Algebra.algHom R A (Localization W))