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

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) : ↥(RingHom.ker g) →ₗ[R] ↥(RingHom.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 : ↥(RingHom.ker g)) : ↑((RingHom.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 (RingHom.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} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Bₚ : Type v') [CommRing 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} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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) : ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f) = ⇑(IsLocalization.map Bₚ f.toRingHom ⋯)

theorem IsLocalization.mapₐ_injective_of_injective {R : Type u} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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 ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)

theorem IsLocalization.mapₐ_surjective_of_surjective {R : Type u} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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 ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)

def AlgHom.toKerIsLocalization {R : Type u} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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)) : (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f) x = (RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯) x

theorem AlgHom.toKerIsLocalization_isLocalizedModule {R : Type u} [CommRing R] (M : Submonoid R) {A : Type v} [CommRing A] [Algebra R A] {B : Type w} [CommRing B] [Algebra R B] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization M Rₚ] (Aₚ : Type v') [CommRing Aₚ] [Algebra R Aₚ] [Algebra A Aₚ] [IsScalarTower R A Aₚ] [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] (Bₚ : Type v') [CommRing 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) (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f)

The canonical linear map from the kernel of an algebra homomorphism to its localization is localizing.