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) : RingHom.ker (map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)

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) : ↥(ker g) →ₛₗ[id R] ↥(ker (IsLocalization.map Q g hy))

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' := ⋯ }

@[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)) : ↑((toKerIsLocalization S Q g hy) r) = (algebraMap R S) ↑r

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) : 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' := ⋯ }

@[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) : ⇑(mapₐ M Rₚ Aₚ Bₚ f) = ⇑(map Bₚ f.toRingHom ⋯)

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)

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) : ↥(RingHom.ker f) →ₗ[A] ↥(RingHom.ker (IsLocalization.mapₐ M Rₚ Aₚ Bₚ f))

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 ⋯

@[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)) : (toKerIsLocalization M Rₚ Aₚ Bₚ f) x = (RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯) x

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.