Localized linear maps

Facts about the localization LocalizedModule.map S f : Mₛ → Nₛ of a linear map at a submonoid S:

• LocalizedModule.map_comp: localization is functorial, (g ∘ f)ₛ = gₛ ∘ fₛ.
• LocalizedModule.bijective_map_lsmul: multiplication by an element of S becomes bijective after localizing at S.
• LocalizedModule.bijective_map_single: the inclusion of a factor of a finite product becomes bijective after localizing at S if every other factor vanishes there.
• LocalizedModule.equivLocalization: the localization of R itself as a module is Localization S, sending mk r s to Localization.mk r s.
• LinearMap.exists_comp_eq_lsmul_of_comp_localizedModule_map_eq_id: if M is finitely presented and N is finitely generated, a left inverse of the localization iₛ of i : N → M descends to a map φ : M → N with φ ∘ i multiplication by some element of S.
• Module.FinitePresentation.exists_bijective_map_of_isLocalizedModule: if M is finitely presented, an isomorphism between localizations of M and N at S gives a map M → N whose localization at S is bijective.
• LocalizedModule.bijective_map_dual_eval_iff: if M and its dual are finitely presented, the map M → M** becomes bijective after localizing at S exactly when the localization Mₛ is reflexive over Rₛ. Taking duals commutes with localization for finitely presented modules, so (M**)ₛ is the double dual of Mₛ over Rₛ.

We also record that localization commutes with dividing by an element:

• TauCeti.localizedQuotSMulTopEquiv: localizing M ⧸ a M gives M_S ⧸ a M_S.

@[simp]

theorem LocalizedModule.map_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : (map S) (g ∘ₗ f) = (map S) g ∘ₗ (map S) f

Localization of a composite is the composite of the localizations.

theorem LocalizedModule.bijective_map_lsmul {R : Type u_1} [CommSemiring R] {S : Submonoid R} (M : Type u_2) [AddCommMonoid M] [Module R M] {s : R} (hs : s ∈ S) : Function.Bijective ⇑((map S) ((LinearMap.lsmul R M) s))

Multiplication by an element of S becomes bijective after localizing at S.

theorem LocalizedModule.bijective_map_single {R : Type u_1} [CommSemiring R] {S : Submonoid R} {ι : Type u_5} [Finite ι] [DecidableEq ι] {E : ι → Type u_6} [(i : ι) → AddCommMonoid (E i)] [(i : ι) → Module R (E i)] (i : ι) (h : ∀ (j : ι), j ≠ i → Subsingleton (LocalizedModule S (E j))) : Function.Bijective ⇑((map S) (LinearMap.single R E i))

Localizing the inclusion E i → ∏ⱼ E j of a factor of a finite product gives a bijection when every other factor vanishes after localizing at S.

noncomputable def LocalizedModule.equivLocalization {R : Type u_1} [CommSemiring R] (S : Submonoid R) : LocalizedModule S R ≃ₗ[Localization S] Localization S

The localization of R at S, as an R-module, is the ring Localization S, linearly over Localization S.

@[simp]

theorem LocalizedModule.equivLocalization_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (r : R) (s : ↥S) : (equivLocalization S) (mk r s) = Localization.mk r s

equivLocalization sends the fraction r / s to the same fraction in Localization S.

@[simp]

theorem LocalizedModule.equivLocalization_symm_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (r : R) (s : ↥S) : (equivLocalization S).symm (Localization.mk r s) = mk r s

The inverse of equivLocalization sends the fraction r / s to the same fraction in LocalizedModule S R.

theorem LinearMap.exists_comp_eq_lsmul_of_comp_localizedModule_map_eq_id {R : Type u_1} [CommRing R] {S : Submonoid R} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.FinitePresentation R M] [Module.Finite R N] (i : N →ₗ[R] M) {ρ : LocalizedModule S M →ₗ[Localization S] LocalizedModule S N} (hρ : ρ ∘ₗ (LocalizedModule.map S) i = id) : ∃ s ∈ S, ∃ (φ : M →ₗ[R] N), φ ∘ₗ i = (lsmul R N) s

Let M be finitely presented and N finitely generated. If the localization of i : N →ₗ[R] M at S has a left inverse, then some φ : M →ₗ[R] N is a left inverse of i up to multiplication by an element of S.

theorem Module.FinitePresentation.exists_bijective_map_of_isLocalizedModule {R : Type u_1} [CommRing R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : N →ₗ[R] N') [IsLocalizedModule S g] [FinitePresentation R M] (l : M' ≃ₗ[R] N') : ∃ (h : M →ₗ[R] N), Function.Bijective ⇑((IsLocalizedModule.map S f g) h)

Let M be finitely presented. An isomorphism l : M' ≃ N' between localizations of M and N at S comes, up to multiplication by an element of S, from a linear map h : M → N; in particular the localization of h is bijective. This is the first step of the proof of Mathlib's Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule.

theorem LocalizedModule.bijective_map_dual_eval_iff {R : Type u_1} [CommRing R] (S : Submonoid R) (Rₛ : Type u_2) [CommRing Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [Module.FinitePresentation R M] [Module.FinitePresentation R (Module.Dual R M)] : Function.Bijective ⇑((map S) (Module.Dual.eval R M)) ↔ Function.Bijective ⇑(Module.Dual.eval Rₛ M')

Let f : M → M' be a localization of M at S, over the localization Rₛ of R. If M and its dual are finitely presented, the canonical map M → M** becomes bijective after localizing at S exactly when M' is reflexive over Rₛ.

noncomputable def TauCeti.localizedQuotSMulTopEquiv {R : Type u} [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] (a : R) (S : Submonoid R) : LocalizedModule S (QuotSMulTop a M) ≃ₗ[Localization S] QuotSMulTop ((algebraMap R (Localization S)) a) (LocalizedModule S M)

Localization commutes with dividing a module by an element: for a : R and a submonoid S, the localization of M ⧸ a M at S is M_S ⧸ a M_S, linearly over R_S.

@[simp]

theorem TauCeti.localizedQuotSMulTopEquiv_mk {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (a : R) (S : Submonoid R) (m : M) (s : ↥S) : (localizedQuotSMulTopEquiv M a S) (LocalizedModule.mk (Submodule.Quotient.mk m) s) = Submodule.Quotient.mk (LocalizedModule.mk m s)

TauCeti.localizedQuotSMulTopEquiv sends (m mod a M) / s to (m / s) mod a M_S.