Localization of algebra maps #
In this file we provide constructors to localize algebra maps. Also we show that localization commutes with taking kernels for ring homomorphisms.
Implementation detail #
The proof that localization commutes with taking kernels does not use the result for linear maps, as the translation is currently tedious and can be unified easily after the localization refactor.
instance
Algebra.idealMap_isLocalizedModule
{R : Type u_1}
(S : Type u_2)
[CommSemiring R]
[CommSemiring S]
(M : Submonoid R)
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
:
IsLocalizedModule M (idealMap S I)
The span of I in a localization of R at M is the localization of I at M.
theorem
IsLocalization.ker_map
{R : Type u_1}
{S : Type u_2}
{P : Type u_3}
(Q : Type u_4)
[CommSemiring R]
[CommSemiring S]
[CommSemiring P]
[CommSemiring Q]
{M : Submonoid R}
{T : Submonoid P}
[Algebra R S]
[Algebra P Q]
[IsLocalization M S]
[IsLocalization T Q]
(g : R →+* P)
(hT : Submonoid.map g M = T)
:
noncomputable def
RingHom.toKerIsLocalization
{R : Type u_1}
(S : Type u_2)
{P : Type u_3}
(Q : Type u_4)
[CommSemiring R]
[CommSemiring S]
[CommSemiring P]
[CommSemiring Q]
{M : Submonoid R}
{T : Submonoid P}
[Algebra R S]
[Algebra P Q]
[IsLocalization M S]
[IsLocalization T Q]
(g : R →+* P)
(hy : M ≤ Submonoid.comap g T)
:
The canonical linear map from the kernel of g to the kernel of its localization.
Equations
- RingHom.toKerIsLocalization S Q g hy = { toFun := fun (x : ↥(RingHom.ker g)) => ⟨(algebraMap R S) ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
RingHom.toKerIsLocalization_apply
{R : Type u_1}
{S : Type u_2}
{P : Type u_3}
(Q : Type u_4)
[CommSemiring R]
[CommSemiring S]
[CommSemiring P]
[CommSemiring Q]
{M : Submonoid R}
{T : Submonoid P}
[Algebra R S]
[Algebra P Q]
[IsLocalization M S]
[IsLocalization T Q]
(g : R →+* P)
(hy : M ≤ Submonoid.comap g T)
(r : ↥(ker g))
:
theorem
RingHom.toKerIsLocalization_isLocalizedModule
{R : Type u_1}
{S : Type u_2}
{P : Type u_3}
(Q : Type u_4)
[CommSemiring R]
[CommSemiring S]
[CommSemiring P]
[CommSemiring Q]
{M : Submonoid R}
{T : Submonoid P}
[Algebra R S]
[Algebra P Q]
[IsLocalization M S]
[IsLocalization T Q]
(g : R →+* P)
(hT : Submonoid.map g M = T)
:
IsLocalizedModule M (toKerIsLocalization S Q g ⋯)
The canonical linear map from the kernel of g to the kernel of its localization
is localizing. In other words, localization commutes with taking kernels.
instance
IsLocalization.isLocalization_algebraMapSubmonoid_map_algHom
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
(f : A →ₐ[R] B)
:
IsLocalization (Submonoid.map f.toRingHom (Algebra.algebraMapSubmonoid A M)) Bₚ
noncomputable def
IsLocalization.mapₐ
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
An algebra map A →ₐ[R] B induces an algebra map on localizations Aₚ →ₐ[Rₚ] Bₚ.
Equations
- IsLocalization.mapₐ M Rₚ Aₚ Bₚ f = { toRingHom := IsLocalization.map Bₚ f.toRingHom ⋯, commutes' := ⋯ }
Instances For
@[simp]
theorem
IsLocalization.mapₐ_coe
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
theorem
IsLocalization.mapₐ_injective_of_injective
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
(hf : Function.Injective ⇑f)
:
Function.Injective ⇑(mapₐ M Rₚ Aₚ Bₚ f)
theorem
IsLocalization.mapₐ_surjective_of_surjective
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
(hf : Function.Surjective ⇑f)
:
Function.Surjective ⇑(mapₐ M Rₚ Aₚ Bₚ f)
theorem
IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
(IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
(IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
f.toLinearMap = (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap
Localizing the underlying linear map of A →ₐ[R] B in the sense of IsLocalizedModule
is the same as taking the underlying linear map of the localization in the sense of
IsLocalization.
theorem
IsLocalization.map_eq_toLinearMap_mapₐ
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
(IsLocalizedModule.map M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap (IsScalarTower.toAlgHom R B Bₚ).toLinearMap)
f.toLinearMap = ↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap
Less linear version of mapExtendScalars_eq_toLinearMap_mapₐ.
For a version where R = A, see map_linearMap_eq_toLinearMap_mapₐ.
theorem
IsLocalization.map_linearMap_eq_toLinearMap_mapₐ
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
[Algebra Rₚ Aₚ]
[IsScalarTower R Rₚ Aₚ]
:
(IsLocalizedModule.map M (Algebra.linearMap R Rₚ) (IsScalarTower.toAlgHom R A Aₚ).toLinearMap) (Algebra.linearMap R A) = ↑R (mapₐ M Rₚ Rₚ Aₚ (Algebra.ofId R A)).toLinearMap
noncomputable def
AlgHom.toKerIsLocalization
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
The canonical linear map from the kernel of an algebra homomorphism to its localization.
Equations
- AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f = RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯
Instances For
@[simp]
theorem
AlgHom.toKerIsLocalization_apply
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
(x : ↥(RingHom.ker f))
:
theorem
AlgHom.toKerIsLocalization_isLocalizedModule
{R : Type u_5}
[CommSemiring R]
(M : Submonoid R)
{A : Type u_6}
[CommSemiring A]
[Algebra R A]
{B : Type u_7}
[CommSemiring B]
[Algebra R B]
(Rₚ : Type u_8)
[CommSemiring Rₚ]
[Algebra R Rₚ]
[IsLocalization M Rₚ]
(Aₚ : Type u_9)
[CommSemiring Aₚ]
[Algebra R Aₚ]
[Algebra A Aₚ]
[IsScalarTower R A Aₚ]
[IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ]
(Bₚ : Type u_10)
[CommSemiring Bₚ]
[Algebra R Bₚ]
[Algebra B Bₚ]
[IsScalarTower R B Bₚ]
[IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ]
[Algebra Rₚ Aₚ]
[Algebra Rₚ Bₚ]
[IsScalarTower R Rₚ Aₚ]
[IsScalarTower R Rₚ Bₚ]
(f : A →ₐ[R] B)
:
IsLocalizedModule (Algebra.algebraMapSubmonoid A M) (toKerIsLocalization M Rₚ Aₚ Bₚ f)
The canonical linear map from the kernel of an algebra homomorphism to its localization is localizing.
theorem
Polynomial.isLocalization
{R : Type u_5}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_6)
[CommSemiring A]
[Algebra R A]
[IsLocalization S A]
:
IsLocalization (Submonoid.map C S) (Polynomial A)
If A is the localization of R at a submonoid S, then A[X] is the localization of
R[X] at S.map Polynomial.C.
See also MvPolynomial.isLocalization for the multivariate case.