Submodules over a localization

This file proves the following facts about submodules and localized modules:

• IsLocalizedModule.mk'_mem_iff: a fraction f x / s lies in a submodule over the localization exactly when f x does.
• Submodule.localized'_one: the localization of the image of A in an algebra B is the image of the localized base ring A' in the localized algebra B'.
• LinearMap.localizedMap_injective_iff_subsingleton_localized_ker: a localized linear map is injective exactly when the localization of its kernel vanishes, the companion of Mathlib's LinearMap.localizedMap_surjective_iff_subsingleton_localized_coker.
• Submodule.FG.exists_smul_mem_of_le_span: clearing denominators uniformly. When F is the localization of R at S, every finitely generated R-submodule of the F-span of an R-submodule M is carried into M by a single element of S. This is the uniform version of Mathlib's multiple_mem_span_of_mem_localization_span.

@[simp]

theorem IsLocalizedModule.mk'_mem_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} {M' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {L : Submodule A M'} {x : M} {s : ↥S} : mk' f x s ∈ L ↔ f x ∈ L

Let A be the localization of R at S, and f : M → M' a localization map at S into an A-module. Then f x / s lies in an A-submodule L of M' exactly when f x does.

@[simp]

theorem Submodule.localized'_one {A : Type u_1} {B : Type u_2} [CommSemiring A] [CommSemiring B] [Algebra A B] (S : Submonoid A) (A' : Type u_3) (B' : Type u_4) [CommSemiring A'] [CommSemiring B'] [Algebra A A'] [IsLocalization S A'] [Algebra B B'] [IsLocalization (Algebra.algebraMapSubmonoid B S) B'] [Algebra A' B'] [Algebra A B'] [IsScalarTower A A' B'] [IsScalarTower A B B'] : localized' A' S (IsScalarTower.toAlgHom A B B').toLinearMap 1 = 1

The localization of the image (1 : Submodule A B) of A in B is the image of A' in B', where A' and B' are the localizations of A at S and of B at the image of S.

theorem Submodule.FG.exists_smul_mem_of_le_span {R : Type u_5} {F : Type u_6} {E : Type u_7} [CommSemiring R] [CommSemiring F] [AddCommMonoid E] [Algebra R F] (S : Submonoid R) [IsLocalization S F] [Module F E] [Module R E] [IsScalarTower R F E] {M N : Submodule R E} (hN : N.FG) (hle : ↑N ⊆ ↑(span F ↑M)) : ∃ r ∈ S, ∀ v ∈ N, r • v ∈ M

Clearing denominators uniformly. If F is the localization of R at S, a finitely generated R-submodule N contained in the F-span of an R-submodule M is carried into M by multiplication by a single element of S.

theorem LinearMap.localizedMap_injective_iff_subsingleton_localized_ker {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) (φ : M →ₗ[R] N) : Function.Injective ⇑((LocalizedModule.map S) φ) ↔ Subsingleton (LocalizedModule S ↥φ.ker)

A localized linear map is injective iff the localization of its kernel vanishes. This is the kernel counterpart of LinearMap.localizedMap_surjective_iff_subsingleton_localized_coker.