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:
- For all
y ∈ M,f yis a unit; - For all
z : S, there exists(x, y) : R × Msuch thatz * f y = f x; - For all
x, y : Rsuch thatf x = f y, there existsc ∈ Msuch thatx * 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: ifQis another localization ofRatM, thenSandQare isomorphic asR-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
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}
:
IsLocalization.mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I
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]
:
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' := ⋯ }
Instances For
@[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)
:
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))
:
AlgHom version of IsLocalization.lift.
Equations
- IsLocalization.liftAlgHom hf = { toRingHom := IsLocalization.lift hf, commutes' := ⋯ }
Instances For
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)
:
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' := ⋯ }
Instances For
@[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
@[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
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)
:
The localization at a module of units is isomorphic to the ring.
Equations
- IsLocalization.atUnits R M H = AlgEquiv.ofBijective (Algebra.ofId R S) ⋯
Instances For
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
Instances For
@[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
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)
:
(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
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) ⟨(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.