Mathlib.RingTheory.Localization.Basic

Module docstring

{"# 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 "}

Localization.mapPiEvalRingHom abbrev

: Localization (S.comap <| Pi.evalRingHom R i) →+* Localization S

Full source

/-- `IsLocalization.map` applied to a projection homomorphism from a product ring. -/
noncomputable abbrev mapPiEvalRingHom :
    LocalizationLocalization (S.comap <| Pi.evalRingHom R i) →+* Localization S :=
  map (T := S) _ (Pi.evalRingHom R i) le_rfl

Induced Homomorphism from Product Localization via Evaluation

Informal description

For a commutative ring $R$ and a submonoid $S$ of $R$, the evaluation homomorphism $\pi_i : R^I \to R$ at index $i$ induces a ring homomorphism from the localization of $R^I$ at $\pi_i^{-1}(S)$ to the localization of $R$ at $S$.

Localization.mapPiEvalRingHom_bijective theorem

: Bijective (mapPiEvalRingHom S)

Full source

theorem mapPiEvalRingHom_bijective : Bijective (mapPiEvalRingHom S) := by
  let T := S.comap (Pi.evalRingHom R i)
  classical
  refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
  · obtain ⟨r₁, s₁, rfl⟩ := mk'_surjective T x₁
    obtain ⟨r₂, s₂, rfl⟩ := mk'_surjective T x₂
    simp_rw [map_mk'] at eq
    rw [IsLocalization.eq] at eq ⊢
    obtain ⟨s, hs⟩ := eq
    refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
    obtain rfl | ne := eq_or_ne j i
    · simpa using hs
    · simp [update_of_ne ne]
  · obtain ⟨r, s, rfl⟩ := mk'_surjective S x
    exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩

Bijectivity of the Evaluation-Induced Localization Map

Informal description

The ring homomorphism $\text{mapPiEvalRingHom}_S$ from the localization of $R^I$ at $\pi_i^{-1}(S)$ to the localization of $R$ at $S$ is bijective, where $\pi_i : R^I \to R$ is the evaluation homomorphism at index $i$.

IsLocalization.linearMap_compatibleSMul theorem

 (N₁ N₂) [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

Full source

theorem linearMap_compatibleSMul (N₁ N₂) [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 where
  map_smul f s s' := by
    obtain ⟨r, m, rfl⟩ := mk'_surjective M s
    rw [← (map_units S m).smul_left_cancel]
    simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]

Compatibility of Linear Maps with Scalar Multiplication in Localized Modules

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be the localization of $R$ at $M$. Suppose $N_1$ and $N_2$ are additive commutative monoids equipped with both $R$-module and $S$-module structures, such that the scalar multiplication actions are compatible via the canonical map $R \to S$ (i.e., $[IsScalarTower\, R\, S\, N_1]$ and $[IsScalarTower\, R\, S\, N_2]$ hold). Then, any linear map between $N_1$ and $N_2$ over $S$ is compatible with the scalar multiplication by elements of $R$.

IsLocalization.algHom_subsingleton theorem

[Algebra R P] : Subsingleton (S →ₐ[R] P)

Full source

theorem algHom_subsingleton [Algebra R P] : Subsingleton (S →ₐ[R] P) :=
  ⟨fun f g =>
    AlgHom.coe_ringHom_injective <|
      IsLocalization.ringHom_ext M <| by rw [f.comp_algebraMap, g.comp_algebraMap]⟩

Uniqueness of Algebra Homomorphisms from Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any commutative ring $P$ equipped with an $R$-algebra structure, there exists at most one $R$-algebra homomorphism from $S$ to $P$.

IsLocalization.algEquiv definition

: S ≃ₐ[R] Q

Full source

/-- If `S`, `Q` are localizations of `R` at the submonoid `M` respectively,
there is an isomorphism of localizations `S ≃ₐ[R] Q`. -/
@[simps!]
noncomputable def algEquiv : S ≃ₐ[R] Q :=
  { ringEquivOfRingEquiv S Q (RingEquiv.refl R) M.map_id with
    commutes' := ringEquivOfRingEquiv_eq _ }

Isomorphism of localizations as $ R $-algebras

Informal description

Given commutative rings $ R $, $ S $, and $ Q $, where $ S $ and $ Q $ are both localizations of $ R $ at the same submonoid $ M $, there exists an $ R $-algebra isomorphism $ S \simeq Q $.

IsLocalization.algEquiv_mk' theorem

(x : R) (y : M) : algEquiv M S Q (mk' S x y) = mk' Q x y

Full source

theorem algEquiv_mk' (x : R) (y : M) : algEquiv M S Q (mk' S x y) = mk' Q x y := by
  simp

Localization Isomorphism Preserves Fraction Construction: $\text{algEquiv}_{M,S,Q}(\text{mk'}_S\, x\, y) = \text{mk'}_Q\, x\, y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $Q$ be localizations of $R$ at $M$. For any $x \in R$ and $y \in M$, the $R$-algebra isomorphism $\text{algEquiv}_{M,S,Q}$ maps the fraction $\text{mk'}_S\, x\, y$ to $\text{mk'}_Q\, x\, y$.

IsLocalization.algEquiv_symm_mk' theorem

(x : R) (y : M) : (algEquiv M S Q).symm (mk' Q x y) = mk' S x y

Full source

theorem algEquiv_symm_mk' (x : R) (y : M) : (algEquiv M S Q).symm (mk' Q x y) = mk' S x y := by simp

Inverse Localization Isomorphism Preserves Fraction Construction: $(\text{algEquiv}_{M,S,Q})^{-1}(\text{mk'}_Q\, x\, y) = \text{mk'}_S\, x\, y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $Q$ be localizations of $R$ at $M$. For any $x \in R$ and $y \in M$, the inverse of the $R$-algebra isomorphism $\text{algEquiv}_{M,S,Q}$ maps the fraction $\text{mk'}_Q\, x\, y$ in $Q$ to the fraction $\text{mk'}_S\, x\, y$ in $S$.

IsLocalization.bijective theorem

(f : S →+* Q) (hf : f.comp (algebraMap R S) = algebraMap R Q) : Function.Bijective f

Full source

protected lemma bijective (f : S →+* Q) (hf : f.comp (algebraMap R S) = algebraMap R Q) :
    Function.Bijective f :=
  (show f = IsLocalization.algEquiv M S Q by
    apply IsLocalization.ringHom_ext M; rw [hf]; ext; simp) ▸
    (IsLocalization.algEquiv M S Q).toEquiv.bijective

Bijectivity of Localization Homomorphisms Preserving Algebra Maps

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ and $Q$ be localizations of $R$ at $M$. For any ring homomorphism $f \colon S \to Q$ such that the composition $f \circ (\text{algebraMap}\, R\, S)$ equals $\text{algebraMap}\, R\, Q$, the map $f$ is bijective.

IsLocalization.liftAlgHom definition

: S →ₐ[A] P

Full source

/-- `AlgHom` version of `IsLocalization.lift`. -/
noncomputable def liftAlgHom : S →ₐ[A] P where
  __ := lift hf
  commutes' r := show lift hf (algebraMap A S r) = _ by
    simp [IsScalarTower.algebraMap_apply A R S]

Algebra homomorphism lift through localization

Informal description

Given a commutative ring $ R $ with a submonoid $ M \subseteq R $, a commutative ring $ S $ that is a localization of $ R $ at $ M $, and a ring homomorphism $ g : R \to P $ such that $ g(y) $ is a unit in $ P $ for every $ y \in M $, the function `IsLocalization.liftAlgHom` constructs an algebra homomorphism from $ S $ to $ P $ that extends $ g $. For any $ z \in S $, this homomorphism sends $ z $ to $ g(x) \cdot (g(y))^{-1} $, where $ (x, y) \in R \times M $ is any pair such that $ z $ is represented as $ f(x) \cdot (f(y))^{-1} $ under the localization map $ f : R \to S $.

IsLocalization.liftAlgHom_toRingHom theorem

: (liftAlgHom hf : S →ₐ[A] P).toRingHom = lift hf

Full source

theorem liftAlgHom_toRingHom : (liftAlgHom hf : S →ₐ[A] P).toRingHom = lift hf := rfl

Underlying Ring Homomorphism of Localization Lift Algebra Homomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. Given a ring homomorphism $g : R \to P$ such that $g(y)$ is a unit in $P$ for every $y \in M$, the underlying ring homomorphism of the algebra homomorphism `liftAlgHom hf` from $S$ to $P$ is equal to the lifted ring homomorphism `lift hf`.

IsLocalization.coe_liftAlgHom theorem

: ⇑(liftAlgHom hf : S →ₐ[A] P) = lift hf

Full source

@[simp]
theorem coe_liftAlgHom : ⇑(liftAlgHom hf : S →ₐ[A] P) = lift hf := rfl

Coefficient Function of Algebra Homomorphism Lift Equals Ring Homomorphism Lift

Informal description

The underlying function of the algebra homomorphism `liftAlgHom hf : S →ₐ[A] P` is equal to the ring homomorphism `lift hf : S →+* P`.

IsLocalization.liftAlgHom_apply theorem

: liftAlgHom hf x = lift hf x

Full source

theorem liftAlgHom_apply : liftAlgHom hf x = lift hf x := rfl

Equality of Algebra Homomorphism Lift and Ring Homomorphism Lift on Localization Elements

Informal description

For any element $x$ in the localization $S$ of a commutative ring $R$ at a submonoid $M$, the algebra homomorphism $\text{liftAlgHom} \ hf$ applied to $x$ is equal to the ring homomorphism $\text{lift} \ hf$ applied to $x$.

IsLocalization.algEquivOfAlgEquiv definition

: S ≃ₐ[A] Q

Full source

/-- 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`. -/
@[simps!]
noncomputable def algEquivOfAlgEquiv : S ≃ₐ[A] Q where
  __ := ringEquivOfRingEquiv S Q h.toRingEquiv H
  commutes' _ := by dsimp; rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]

Isomorphism of localizations induced by an algebra isomorphism

Informal description

Given commutative rings $ R $ and $ P $ with submonoids $ M \subseteq R $ and $ T \subseteq P $, and localizations $ S $ of $ R $ at $ M $ and $ Q $ of $ P $ at $ T $, an algebra isomorphism $ h : R \simeq_{\!\!A} P $ such that $ h(M) = T $ induces an algebra isomorphism $ S \simeq_{\!\!A} Q $.

IsLocalization.algEquivOfAlgEquiv_eq_map theorem

: (algEquivOfAlgEquiv S Q h H : S →+* Q) = map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H))

Full source

theorem algEquivOfAlgEquiv_eq_map :
    (algEquivOfAlgEquiv S Q h H : S →+* Q) =
      map Q (h : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) :=
  rfl

Equality of Localization Isomorphism and Induced Map via Algebra Isomorphism

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given an algebra isomorphism $h : R \simeq_{\!\!A} P$ such that $h(M) = T$, the induced algebra isomorphism $\text{algEquivOfAlgEquiv} \ S \ Q \ h \ H : S \simeq_{\!\!A} Q$ coincides with the ring homomorphism $\text{map} \ Q \ h$ obtained from the inclusion $M \subseteq h^{-1}(T)$.

IsLocalization.algEquivOfAlgEquiv_eq theorem

(x : R) : algEquivOfAlgEquiv S Q h H ((algebraMap R S) x) = algebraMap P Q (h x)

Full source

theorem algEquivOfAlgEquiv_eq (x : R) :
    algEquivOfAlgEquiv S Q h H ((algebraMap R S) x) = algebraMap P Q (h x) := by
  simp

Compatibility of Localization Isomorphism with Algebra Maps

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given an algebra isomorphism $h : R \simeq_{\!\!A} P$ such that $h(M) = T$, the induced isomorphism $\text{algEquivOfAlgEquiv}\, S\, Q\, h\, H : S \simeq_{\!\!A} Q$ satisfies $\text{algEquivOfAlgEquiv}\, S\, Q\, h\, H (\text{algebraMap}\, R\, S\, x) = \text{algebraMap}\, P\, Q (h x)$ for every $x \in R$.

IsLocalization.algEquivOfAlgEquiv_mk' theorem

 (x : R) (y : M) :
  algEquivOfAlgEquiv S Q h H (mk' S x y) = mk' Q (h x) ⟨h y, show h y ∈ T from H ▸ Set.mem_image_of_mem h y.2⟩

Full source

theorem algEquivOfAlgEquiv_mk' (x : R) (y : M) :
    algEquivOfAlgEquiv S Q h H (mk' S x y) =
      mk' Q (h x) ⟨h y, show h y ∈ T from H ▸ Set.mem_image_of_mem h y.2⟩ := by
  simp [map_mk']

Localization Isomorphism Preserves Fraction Construction: $\text{algEquivOfAlgEquiv}\, S\, Q\, h\, H\, (\text{mk'}_S\, x\, y) = \text{mk'}_Q\, (h x)\, \langle h y, y.2 \rangle$

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given an algebra isomorphism $h : R \simeq_{\!\!A} P$ such that $h(M) = T$, the induced algebra isomorphism $\text{algEquivOfAlgEquiv}\, S\, Q\, h\, H : S \simeq_{\!\!A} Q$ satisfies the following property: for any $x \in R$ and $y \in M$, the image of the fraction $\text{mk'}_S\, x\, y$ under this isomorphism equals $\text{mk'}_Q\, (h x)\, \langle h y, y.2 \rangle$, where $\text{mk'}_S$ and $\text{mk'}_Q$ construct elements in the localizations $S$ and $Q$ respectively.

IsLocalization.algEquivOfAlgEquiv_symm theorem

 :
  (algEquivOfAlgEquiv S Q h H).symm =
    algEquivOfAlgEquiv Q S h.symm
      (show Submonoid.map h.symm T = M by
        rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv, ← Submonoid.comap_equiv_eq_map_symm, ←
          Submonoid.map_coe_toMulEquiv, Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective])

Full source

theorem algEquivOfAlgEquiv_symm : (algEquivOfAlgEquiv S Q h H).symm =
    algEquivOfAlgEquiv Q S h.symm (show Submonoid.map h.symm T = M by
      rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]) := rfl

Inverse of Localization Isomorphism Induced by Algebra Isomorphism

Informal description

Let $R$ and $P$ be commutative rings with submonoids $M \subseteq R$ and $T \subseteq P$ respectively, and let $S$ and $Q$ be localizations of $R$ at $M$ and $P$ at $T$ respectively. Given an algebra isomorphism $h : R \simeq_{\!\!A} P$ such that $h(M) = T$, the inverse of the induced algebra isomorphism $\text{algEquivOfAlgEquiv} : S \simeq_{\!\!A} Q$ is equal to the algebra isomorphism $\text{algEquivOfAlgEquiv} : Q \simeq_{\!\!A} S$ induced by $h^{-1} : P \simeq_{\!\!A} R$ and the equality $\text{Submonoid.map } h^{-1} T = M$.

IsLocalization.atUnits definition

(H : M ≤ IsUnit.submonoid R) : R ≃ₐ[R] S

Full source

/-- The localization at a module of units is isomorphic to the ring. -/
noncomputable def atUnits (H : M ≤ IsUnit.submonoid R) : R ≃ₐ[R] S := by
  refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩
  · intro x y hxy
    obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
    obtain ⟨u, hu⟩ := H c.prop
    rwa [← hu, Units.mul_right_inj] at eq
  · intro y
    obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
    obtain ⟨u, hu⟩ := H s.prop
    use x * u.inv
    dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
    rw [RingHom.map_mul, ← eq, ← hu, mul_assoc, ← RingHom.map_mul]
    simp

Localization at units is isomorphic to the base ring

Informal description

Given a commutative ring $ R $ and a submonoid $ M $ of $ R $ consisting entirely of units (i.e., $ M \leq \text{IsUnit.submonoid } R $), the localization $ S $ of $ R $ at $ M $ is isomorphic to $ R $ as an $ R $-algebra. More precisely, the canonical algebra homomorphism $ R \to S $ is a bijective $ R $-algebra homomorphism, hence an isomorphism.

IsLocalization.isLocalization_of_algEquiv theorem

[Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) : IsLocalization M P

Full source

theorem isLocalization_of_algEquiv [Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) :
    IsLocalization M P := by
  constructor
  · intro y
    convert (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom
    exact (h.commutes y).symm
  · intro y
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
    apply_fun (show S → P from h) at e
    simp only [map_mul, h.apply_symm_apply, h.commutes] at e
    exact ⟨⟨x, s⟩, e⟩
  · intro x y
    rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
      h.symm.commutes]
    exact id

Localization Property Preserved under Algebra Isomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $P$ be $R$-algebras. Suppose $S$ is the localization of $R$ at $M$ and $h : S \simeq_{\text{Alg}[R]} P$ is an $R$-algebra isomorphism. Then $P$ is also a localization of $R$ at $M$.

IsLocalization.isLocalization_iff_of_algEquiv theorem

[Algebra R P] (h : S ≃ₐ[R] P) : IsLocalization M S ↔ IsLocalization M P

Full source

theorem isLocalization_iff_of_algEquiv [Algebra R P] (h : S ≃ₐ[R] P) :
    IsLocalizationIsLocalization M S ↔ IsLocalization M P :=
  ⟨fun _ => isLocalization_of_algEquiv M h, fun _ => isLocalization_of_algEquiv M h.symm⟩

Localization Characterization via Algebra Isomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $P$ be $R$-algebras. Given an $R$-algebra isomorphism $h : S \simeq_{\text{Alg}[R]} P$, the following are equivalent: 1. $S$ is the localization of $R$ at $M$; 2. $P$ is the localization of $R$ at $M$.

IsLocalization.isLocalization_iff_of_ringEquiv theorem

 (h : S ≃+* P) :
  IsLocalization M S ↔
    haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra;
    IsLocalization M P

Full source

theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) :
    IsLocalizationIsLocalization M S ↔
      haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra; IsLocalization M P :=
  letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra
  isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl }

Localization Characterization via Ring Isomorphism

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ and $P$ be commutative rings. Given a ring isomorphism $h : S \simeq P$, the following are equivalent: 1. $S$ is the localization of $R$ at $M$; 2. With the $R$-algebra structure on $P$ induced by $h \circ \text{algebraMap } R S$, the ring $P$ is the localization of $R$ at $M$.

IsLocalization.isLocalization_iff_of_isLocalization theorem

[IsLocalization M S] [IsLocalization N S] [Algebra R P] : IsLocalization M P ↔ IsLocalization N P

Full source

/-- 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_isLocalization [IsLocalization M S] [IsLocalization N S]
    [Algebra R P] : IsLocalizationIsLocalization M P ↔ IsLocalization N P :=
  ⟨fun _ ↦ isLocalization_of_algEquiv N (algEquiv M S P),
    fun _ ↦ isLocalization_of_algEquiv M (algEquiv N S P)⟩

Equivalence of Localizations at Different Submonoids When Shared Localization Exists

Informal description

Let $R$ be a commutative ring with submonoids $M$ and $N$, and let $S$ and $P$ be $R$-algebras. Suppose $S$ is simultaneously a localization of $R$ at both $M$ and $N$. Then for any $R$-algebra $P$, the following are equivalent: 1. $P$ is a localization of $R$ at $M$; 2. $P$ is a localization of $R$ at $N$.

IsLocalization.iff_of_le_of_exists_dvd theorem

 (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) : IsLocalization M S ↔ IsLocalization N S

Full source

theorem iff_of_le_of_exists_dvd (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m) :
    IsLocalizationIsLocalization M S ↔ IsLocalization N S :=
  have : IsLocalization N (Localization M) := of_le_of_exists_dvd _ _ h₁ h₂
  isLocalization_iff_of_isLocalization _ _ (Localization M)

Equivalence of Localizations at Nested Submonoids with Divisibility Condition

Informal description

Let $R$ be a commutative ring with submonoids $M$ and $N$ such that $M \subseteq N$. Suppose that for every $n \in N$, there exists $m \in M$ such that $n$ divides $m$. Then for any commutative ring $S$, the following are equivalent: 1. $S$ is a localization of $R$ at $M$; 2. $S$ is a localization of $R$ at $N$.

IsLocalization.commutes theorem

 (S₁ S₂ T : Type*) [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

Full source

/-- 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`. -/
lemma commutes (S₁ S₂ T : Type*) [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 where
  map_units' := by
    rintro ⟨m, ⟨a, ha, rfl⟩⟩
    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]
    exact IsUnit.map _ (IsLocalization.map_units' ⟨a, ha⟩)
  surj' a := by
    obtain ⟨⟨y, -, m, hm, rfl⟩, hy⟩ := surj (M := Algebra.algebraMapSubmonoid S₂ M₁) a
    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₁ T] at hy
    obtain ⟨⟨z, n, hn⟩, hz⟩ := IsLocalization.surj (M := M₂) y
    have hunit : IsUnit (algebraMap R S₁ m) := map_units' ⟨m, hm⟩
    use ⟨algebraMap R S₁ z * hunit.unit⁻¹, ⟨algebraMap R S₁ n, n, hn, rfl⟩⟩
    rw [map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]
    conv_rhs => rw [← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply R S₂ T, ← hz, map_mul, ← hy]
    convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)
    · rw [map_mul]
      ring
    simp
  exists_of_eq {x y} hxy := by
    obtain ⟨r, s, d, hr, hs⟩ := IsLocalization.surj₂ M₁ S₁ x y
    apply_fun (· * algebraMap S₁ T (algebraMap R S₁ d)) at hxy
    simp_rw [← map_mul, hr, hs, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R S₂ T] at hxy
    obtain ⟨⟨-, c, hmc, rfl⟩, hc⟩ := exists_of_eq (M := Algebra.algebraMapSubmonoid S₂ M₁) hxy
    simp_rw [← map_mul] at hc
    obtain ⟨a, ha⟩ := IsLocalization.exists_of_eq (M := M₂) hc
    use ⟨algebraMap R S₁ a, a, a.property, rfl⟩
    apply (map_units S₁ d).mul_right_cancel
    rw [mul_assoc, hr, mul_assoc, hs]
    apply (map_units S₁ ⟨c, hmc⟩).mul_right_cancel
    rw [← map_mul, ← map_mul, mul_assoc, mul_comm _ c, ha, map_mul, map_mul]
    ring

Commutativity of Localizations: $M_1^{-1}M_2^{-1}R \cong M_2^{-1}M_1^{-1}R$

Informal description

Let $R$ be a commutative ring with submonoids $M_1$ and $M_2$, and let $S_1$ and $S_2$ be localizations of $R$ at $M_1$ and $M_2$ respectively. Let $T$ be a commutative ring that is both: 1. A localization of $S_2$ at the image of $M_1$ under the algebra map $R \to S_2$ (denoted $\text{algebraMapSubmonoid}\, S_2\, M_1$), and 2. An algebra over both $S_1$ and $S_2$ with compatible scalar tower structures. Then $T$ is also a localization of $S_1$ at the image of $M_2$ under the algebra map $R \to S_1$ (denoted $\text{algebraMapSubmonoid}\, S_1\, M_2$).

Localization.mk_natCast theorem

(m : ℕ) : (mk m 1 : Localization M) = m

Full source

theorem mk_natCast (m : ℕ) : (mk m 1 : Localization M) = m := by
  simpa using mk_algebraMap (R := R) (A := ℕ) _

Localization of Natural Number at Identity Equals Itself

Informal description

For any natural number $m$ and any submonoid $M$ of a commutative ring $R$, the localization of $m$ at the identity element $1 \in M$ is equal to $m$ itself, i.e., $\text{mk}(m, 1) = m$ in the localization $R[M^{-1}]$.

Localization.algEquiv definition

: Localization M ≃ₐ[R] S

Full source

/-- The localization of `R` at `M` as a quotient type is isomorphic to any other localization. -/
@[simps!]
noncomputable def algEquiv : LocalizationLocalization M ≃ₐ[R] S :=
  IsLocalization.algEquiv M _ _

Isomorphism of localizations as $ R $-algebras

Informal description

The localization of a commutative ring $ R $ at a submonoid $ M $, denoted $ R[M^{-1}] $, is isomorphic as an $ R $-algebra to any other localization $ S $ of $ R $ at $ M $.

IsLocalization.unique definition

 (R Rₘ) [CommSemiring R] [CommSemiring Rₘ] (M : Submonoid R) [Subsingleton R] [Algebra R Rₘ] [IsLocalization M Rₘ] :
  Unique Rₘ

Full source

/-- The localization of a singleton is a singleton. Cannot be an instance due to metavariables. -/
noncomputable def _root_.IsLocalization.unique (R Rₘ) [CommSemiring R] [CommSemiring Rₘ]
    (M : Submonoid R) [Subsingleton R] [Algebra R Rₘ] [IsLocalization M Rₘ] : Unique Rₘ :=
  have : Inhabited Rₘ := ⟨1⟩
  (algEquiv M Rₘ).symm.injective.unique

Uniqueness of localization of a singleton ring

Informal description

If $ R $ is a commutative semiring with exactly one element (i.e., a subsingleton), then any localization $ R_M $ of $ R $ at a submonoid $ M $ also has exactly one element (i.e., is `Unique`). This follows from the fact that the algebra isomorphism between $ R_M $ and any other localization of $ R $ at $ M $ is injective, and thus preserves the uniqueness property.

Localization.algEquiv_mk' theorem

(x : R) (y : M) : algEquiv M S (mk' (Localization M) x y) = mk' S x y

Full source

nonrec theorem algEquiv_mk' (x : R) (y : M) : algEquiv M S (mk' (Localization M) x y) = mk' S x y :=
  algEquiv_mk' _ _

Localization isomorphism preserves fraction construction: $\text{algEquiv}_{M,S}(\text{mk'}_{R[M^{-1}]}(x, y)) = \text{mk'}_S(x, y)$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any $x \in R$ and $y \in M$, the $R$-algebra isomorphism $\text{algEquiv}_{M,S}$ between the standard localization $R[M^{-1}]$ and $S$ maps the fraction $\text{mk'}_{R[M^{-1}]}(x, y)$ to $\text{mk'}_S(x, y)$.

Localization.algEquiv_symm_mk' theorem

(x : R) (y : M) : (algEquiv M S).symm (mk' S x y) = mk' (Localization M) x y

Full source

nonrec theorem algEquiv_symm_mk' (x : R) (y : M) :
    (algEquiv M S).symm (mk' S x y) = mk' (Localization M) x y :=
  algEquiv_symm_mk' _ _

Inverse Localization Isomorphism Preserves Fraction Construction: $(\text{algEquiv}_{M,S})^{-1}(\text{mk'}_S\, x\, y) = \text{mk'}_{R[M^{-1}]}\, x\, y$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $S$ be a localization of $R$ at $M$. For any $x \in R$ and $y \in M$, the inverse of the $R$-algebra isomorphism $\text{algEquiv}_{M,S}$ maps the fraction $\text{mk'}_S(x, y)$ in $S$ to the fraction $\text{mk'}_{R[M^{-1}]}(x, y)$ in the standard localization $R[M^{-1}]$.

Localization.algEquiv_mk theorem

(x y) : algEquiv M S (mk x y) = mk' S x y

Full source

theorem algEquiv_mk (x y) : algEquiv M S (mk x y) = mk' S x y := by rw [mk_eq_mk', algEquiv_mk']

Localization isomorphism maps standard fractions to target fractions: $\text{algEquiv}_{M,S}(\text{mk}(x, y)) = \text{mk'}_S(x, y)$

Informal description

Localization.algEquiv_symm_mk theorem

(x : R) (y : M) : (algEquiv M S).symm (mk' S x y) = mk x y

Full source

theorem algEquiv_symm_mk (x : R) (y : M) : (algEquiv M S).symm (mk' S x y) = mk x y := by
  rw [mk_eq_mk', algEquiv_symm_mk']

Inverse Localization Isomorphism Maps Fractions to Standard Form: $(\text{algEquiv}_{M,S})^{-1}(\text{mk'}_S\, x\, y) = \text{mk}(x, y)$

Informal description

Localization.coe_algEquiv theorem

: (Localization.algEquiv M S : Localization M →+* S) = IsLocalization.map (M := M) (T := M) _ (RingHom.id R) le_rfl

Full source

lemma coe_algEquiv :
    (Localization.algEquiv M S : LocalizationLocalization M →+* S) =
    IsLocalization.map (M := M) (T := M) _ (RingHom.id R) le_rfl := rfl

Ring homomorphism component of localization isomorphism equals induced map

Informal description

The ring homomorphism component of the $R$-algebra isomorphism $\text{Localization.algEquiv} : R[M^{-1}] \simeq S$ is equal to the induced homomorphism $\text{IsLocalization.map}$ from $R[M^{-1}]$ to $S$ corresponding to the identity map $\text{RingHom.id} : R \to R$ and the trivial inclusion $M \subseteq M$.

Localization.coe_algEquiv_symm theorem

 :
  ((Localization.algEquiv M S).symm : S →+* Localization M) =
    IsLocalization.map (M := M) (T := M) _ (RingHom.id R) le_rfl

Full source

lemma coe_algEquiv_symm :
    ((Localization.algEquiv M S).symm : S →+* Localization M) =
    IsLocalization.map (M := M) (T := M) _ (RingHom.id R) le_rfl := rfl

Inverse of Localization Isomorphism Equals Induced Map

Informal description

The inverse of the $R$-algebra isomorphism $\text{Localization.algEquiv}\, M\, S : R[M^{-1}] \simeq S$ is equal to the ring homomorphism $\text{IsLocalization.map}\, (M := M)\, (T := M)\, \text{id}_R\, \text{le\_rfl}$ from $S$ to $R[M^{-1}]$, where $\text{id}_R$ is the identity map on $R$ and $\text{le\_rfl}$ is the proof that $M$ is contained in itself under the identity map.

Localization.mk_intCast theorem

(m : ℤ) : (mk m 1 : Localization M) = m

Full source

theorem mk_intCast (m : ℤ) : (mk m 1 : Localization M) = m := by
  simpa using mk_algebraMap (R := R) (A := ℤ) _

Localization of Integer at Identity Equals Itself

Informal description

For any integer $m \in \mathbb{Z}$, the localization of $m$ at the identity element $1$ in the submonoid $M$ is equal to $m$ itself, i.e., $\text{mk}(m, 1) = m$ in the localization $R[M^{-1}]$.

IsField.localization_map_bijective theorem

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

Full source

/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
theorem IsField.localization_map_bijective {R Rₘ : Type*} [CommRing R] [CommRing Rₘ]
    {M : Submonoid R} (hM : (0 : R) ∉ M) (hR : IsField R) [Algebra R Rₘ] [IsLocalization M Rₘ] :
    Function.Bijective (algebraMap R Rₘ) := by
  letI := hR.toField
  replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
  refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩
  obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x
  obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)
  exact ⟨r * n, by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩

Bijectivity of Localization Map for Fields

Informal description

Let $R$ be a commutative ring that is a field, $M$ a submonoid of $R$ not containing $0$, and $R_M$ the localization of $R$ at $M$. Then the canonical algebra map $\text{algebraMap}\, R\, R_M$ is bijective.

Field.localization_map_bijective theorem

 {K Kₘ : Type*} [Field K] [CommRing Kₘ] {M : Submonoid K} (hM : (0 : K) ∉ M) [Algebra K Kₘ] [IsLocalization M Kₘ] :
  Function.Bijective (algebraMap K Kₘ)

Full source

/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
theorem Field.localization_map_bijective {K Kₘ : Type*} [Field K] [CommRing Kₘ] {M : Submonoid K}
    (hM : (0 : K) ∉ M) [Algebra K Kₘ] [IsLocalization M Kₘ] :
    Function.Bijective (algebraMap K Kₘ) :=
  (Field.toIsField K).localization_map_bijective hM

Bijectivity of Localization Map for Fields

Informal description

Let $K$ be a field, $M$ a submonoid of $K$ not containing $0$, and $K_M$ the localization of $K$ at $M$. Then the canonical algebra homomorphism $\text{algebraMap}\, K\, K_M$ is bijective.

localizationAlgebra definition

: Algebra Rₘ Sₘ

Full source

/-- 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.
-/
noncomputable def localizationAlgebra : Algebra Rₘ Sₘ :=
  (map Sₘ (algebraMap R S)
        (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :
      Rₘ →+* Sₘ).toAlgebra

Natural algebra structure on localizations induced by an algebra map

Informal description

Given a commutative ring $ R $ with a submonoid $ M $, and localizations $ R_M $ of $ R $ at $ M $ and $ S_M $ of $ S $ at the image of $ M $ under the algebra map $ R \to S $, the algebra structure `localizationAlgebra` equips $ R_M \to S_M $ with the natural algebra structure such that the following diagram commutes: \[ \begin{array}{ccc} R & \longrightarrow & S \\ \downarrow & & \downarrow \\ R_M & \longrightarrow & S_M \end{array} \] Here, the vertical maps are the localization maps, and the horizontal maps are the given algebra maps. The commutativity of the diagram is ensured by the construction of the algebra structure.

IsLocalization.map_units_map_submonoid theorem

(y : M) : IsUnit (algebraMap R Sₘ y)

Full source

theorem IsLocalization.map_units_map_submonoid (y : M) : IsUnit (algebraMap R Sₘ y) := by
  rw [IsScalarTower.algebraMap_apply _ S]
  exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Images of Submonoid Elements are Units in Localization

Informal description

For any element $y$ in the submonoid $M$ of a commutative ring $R$, the image of $y$ under the canonical ring homomorphism $\text{algebraMap}\, R\, S_\mu : R \to S_\mu$ is a unit in the localization $S_\mu$.

IsLocalization.algebraMap_mk' theorem

 (x : R) (y : M) :
  algebraMap Rₘ Sₘ (IsLocalization.mk' Rₘ x y) =
    IsLocalization.mk' Sₘ (algebraMap R S x) ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Full source

theorem IsLocalization.algebraMap_mk' (x : R) (y : M) :
    algebraMap Rₘ Sₘ (IsLocalization.mk' Rₘ x y) =
      IsLocalization.mk' Sₘ (algebraMap R S x)
        ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩ := by
  rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
    IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
    IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← map_mul, mul_comm,
    IsLocalization.mul_mk'_eq_mk'_of_mul]
  exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

Compatibility of Algebra Map with Localization Construction: $\text{algebraMap}\, R_M\, S_M\, (\text{mk'}\, R_M\, x\, y) = \text{mk'}\, S_M\, (\text{algebraMap}\, R\, S\, x)\, \langle \text{algebraMap}\, R\, S\, y, \text{mem\_algebraMapSubmonoid\_of\_mem}\, y \rangle$

Informal description

Let $R$ be a commutative ring with a submonoid $M$, and let $R_M$ and $S_M$ be the localizations of $R$ and $S$ at $M$ and the image of $M$ under the algebra map $R \to S$, respectively. For any $x \in R$ and $y \in M$, the algebra map $\text{algebraMap}\, R_M\, S_M$ applied to the localized element $\text{mk'}\, R_M\, x\, y$ equals the localized element $\text{mk'}\, S_M\, (\text{algebraMap}\, R\, S\, x)\, \langle \text{algebraMap}\, R\, S\, y, \text{Algebra.mem\_algebraMapSubmonoid\_of\_mem}\, y \rangle$.

IsLocalization.algebraMap_eq_map_map_submonoid theorem

 : algebraMap Rₘ Sₘ = map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map)

Full source

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
theorem IsLocalization.algebraMap_eq_map_map_submonoid :
    algebraMap Rₘ Sₘ =
      map Sₘ (algebraMap R S)
        (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :=
  Eq.symm <|
    IsLocalization.map_unique _ (algebraMap Rₘ Sₘ) fun x => by
      rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

Equality of Canonical and Induced Localization Maps

Informal description

The canonical algebra homomorphism from the localization $R_M$ to the localization $S_M$ is equal to the induced localization map obtained by applying the algebra homomorphism $\text{algebraMap}\, R\, S$ to $R_M$, where the submonoid condition $M \leq (\text{algebraMapSubmonoid}\, S\, M).\text{comap}\, (\text{algebraMap}\, R\, S)$ holds by the inclusion $M \subseteq f^{-1}(f(M))$ for $f = \text{algebraMap}\, R\, S$.

IsLocalization.algebraMap_apply_eq_map_map_submonoid theorem

 (x) :
  algebraMap Rₘ Sₘ x =
    map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) x

Full source

/-- If the square below commutes, the bottom map is uniquely specified:
```
R  →  S
↓     ↓
Rₘ → Sₘ
```
-/
theorem IsLocalization.algebraMap_apply_eq_map_map_submonoid (x) :
    algebraMap Rₘ Sₘ x =
      map Sₘ (algebraMap R S)
        (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) x :=
  DFunLike.congr_fun (IsLocalization.algebraMap_eq_map_map_submonoid _ _ _ _) x

Pointwise Equality of Canonical and Induced Localization Maps

Informal description

For any element $x$ in the localization $R_M$ of a commutative ring $R$ at a submonoid $M$, the algebra homomorphism $\text{algebraMap}\, R_M\, S_M$ applied to $x$ is equal to the induced map $\text{map}\, S_M\, (\text{algebraMap}\, R\, S)$ applied to $x$, where the submonoid condition $M \leq (\text{algebraMapSubmonoid}\, S\, M).\text{comap}\, (\text{algebraMap}\, R\, S)$ holds by the inclusion $M \subseteq f^{-1}(f(M))$ for $f = \text{algebraMap}\, R\, S$.

IsLocalization.lift_algebraMap_eq_algebraMap theorem

: IsLocalization.lift (M := M) (IsLocalization.map_units_map_submonoid S Sₘ) = algebraMap Rₘ Sₘ

Full source

theorem IsLocalization.lift_algebraMap_eq_algebraMap :
    IsLocalization.lift (M := M) (IsLocalization.map_units_map_submonoid S Sₘ) =
      algebraMap Rₘ Sₘ :=
  IsLocalization.lift_unique _ fun _ => (IsScalarTower.algebraMap_apply _ _ _ _).symm

Lift of Canonical Algebra Map Equals Canonical Algebra Map in Localization

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be a localization of $R$ at $M$. The homomorphism obtained by lifting the canonical algebra map $R \to S$ through the localization at $M$ is equal to the canonical algebra map from the localization $R_M$ to $S_M$.

localizationAlgebraMap_def theorem

 :
  @algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S) =
    map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map)

Full source

theorem localizationAlgebraMap_def :
    @algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S) =
      map Sₘ (algebraMap R S)
        (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :=
  rfl

Equality of Localization Algebra Maps

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be an $R$-algebra. Let $R_M$ and $S_M$ be the localizations of $R$ and $S$ at $M$ and the image of $M$ under the algebra map $R \to S$, respectively. Then the algebra map $\text{algebraMap}_{R_M} S_M$ from $R_M$ to $S_M$ induced by the localization algebra structure equals the map induced by the algebra map $R \to S$ and the inclusion $M \subseteq f^{-1}(f(M))$, where $f$ is the algebra map $R \to S$.

localizationAlgebra_injective theorem

(hRS : Function.Injective (algebraMap R S)) : Function.Injective (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S))

Full source

/-- Injectivity of the underlying `algebraMap` descends to the algebra induced by localization. -/
theorem localizationAlgebra_injective (hRS : Function.Injective (algebraMap R S)) :
    Function.Injective (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) :=
  have : IsLocalization (M.map (algebraMap R S)) Sₘ := i
  IsLocalization.map_injective_of_injective _ _ _ hRS

Injectivity of Localization-Induced Algebra Map Preserved from Base Algebra Map

Informal description

Let $R$ be a commutative ring with a submonoid $M \subseteq R$, and let $S$ be an $R$-algebra. If the algebra map $\text{algebraMap}\, R\, S$ is injective, then the induced algebra map $\text{algebraMap}\, R_M\, S_M$ between the localizations of $R$ at $M$ and $S$ at the image of $M$ under $\text{algebraMap}\, R\, S$ is also injective.