Localizing a localization map

Let f : M → M' and f₂ : N → N' be localizations at a submonoid S. If a scalar r acts invertibly on M, it acts invertibly on M', because the action of r on M' is the map induced by the action of r on M. Consequently, if g : M → N is a localization at a second submonoid T, then so is the induced map M' → N': localizations at S and at T commute. For the module of sections of a quasi-coherent sheaf this says that restricting from D(s) to D(s t) is a localization away from t.

Main statements

• IsLocalizedModule.isUnit_algebraMap_of_isUnit: invertible scalars stay invertible on a localization.
• IsLocalizedModule.isLocalizedModule_map: the map induced on localizations at S by a localization at T is a localization at T.
• IsLocalizedModule.of_bijective_semilinearMap: a linear map identified, along a ring homomorphism σ : R →+* A, with a localization at the image of S is a localization at S.

theorem IsLocalizedModule.isUnit_algebraMap_of_isUnit {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {r : R} (h : IsUnit ((algebraMap R (Module.End R M)) r)) : IsUnit ((algebraMap R (Module.End R M')) r)

A scalar acting invertibly on a module acts invertibly on each of its localizations.

theorem IsLocalizedModule.isLocalizedModule_map {R : Type u_1} [CommSemiring R] (S : Submonoid R) {T : Submonoid R} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {N' : Type u_5} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid N] [AddCommMonoid N'] [Module R M] [Module R M'] [Module R N] [Module R N'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (f₂ : N →ₗ[R] N') [IsLocalizedModule S f₂] (g : M →ₗ[R] N) [IsLocalizedModule T g] : IsLocalizedModule T ((map S f f₂) g)

Localizations at two submonoids commute: if g : M → N is a localization at T, then the map induced by g between localizations at S is again a localization at T.

theorem IsLocalizedModule.of_bijective_semilinearMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) {A : Type u_6} [CommSemiring A] {σ : R →+* A} {M : Type u_7} {N : Type u_8} {M' : Type u_9} {N' : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M'] [AddCommMonoid N'] [Module R M] [Module R N] [Module A M'] [Module A N'] (f : M →ₗ[R] N) (f' : M' →ₗ[A] N') [IsLocalizedModule (Submonoid.map σ S) f'] (eM : M →ₛₗ[σ] M') (eN : N →ₛₗ[σ] N') (heM : Function.Bijective ⇑eM) (heN : Function.Bijective ⇑eN) (h : ∀ (x : M), eN (f x) = f' (eM x)) : IsLocalizedModule S f

Localizations transported along semilinear bijections. Let σ : R →+* A be a ring homomorphism, f : M →ₗ[R] N an R-linear map and f' : M' →ₗ[A] N' an A-linear map which is a localization at the image S.map σ. If f corresponds to f' under σ-semilinear bijections M → M' and N → N', then f is a localization at S.