Detecting injectivity at associated primes

An R-linear map between arbitrary modules over a Noetherian commutative ring is injective if its localization is injective at every associated prime of its domain.

References

• Stacks Project, Lemma 15.24.12 (Tag 0AV7).

theorem LinearMap.injective_of_isLocalized_associatedPrimes {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (map : M →ₗ[R] N) (Mₚ : ↑(associatedPrimes R M) → Type u_4) [(prime : ↑(associatedPrimes R M)) → AddCommMonoid (Mₚ prime)] [(prime : ↑(associatedPrimes R M)) → Module R (Mₚ prime)] (f : (prime : ↑(associatedPrimes R M)) → M →ₗ[R] Mₚ prime) [∀ (prime : ↑(associatedPrimes R M)), IsLocalizedModule (↑prime).primeCompl (f prime)] (Nₚ : ↑(associatedPrimes R M) → Type u_5) [(prime : ↑(associatedPrimes R M)) → AddCommMonoid (Nₚ prime)] [(prime : ↑(associatedPrimes R M)) → Module R (Nₚ prime)] (g : (prime : ↑(associatedPrimes R M)) → N →ₗ[R] Nₚ prime) (F : (prime : ↑(associatedPrimes R M)) → Mₚ prime →ₗ[R] Nₚ prime) (commutes : ∀ (prime : ↑(associatedPrimes R M)), F prime ∘ₗ f prime = g prime ∘ₗ map) (local_injective : ∀ (prime : ↑(associatedPrimes R M)), Function.Injective ⇑(F prime)) : Function.Injective ⇑map

A linear map is injective if, at every associated prime of its domain, a compatible map from a localization of the domain is injective. Neither module needs to be finitely generated, and the target of the compatible map need not itself be a localization. The base may be a commutative semiring when the source module has an additive group.

theorem LinearMap.injective_of_forall_localization_of_addCommGroup {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (map : M →ₗ[R] N) (local_injective : ∀ (prime : Ideal R) [inst : prime.IsPrime], Function.Injective ⇑((LocalizedModule.map prime.primeCompl) map) ∨ prime ∉ associatedPrimes R M) : Function.Injective ⇑map

A linear map from an additive group over a commutative semiring is injective if its localization is injective at every associated prime of its domain.

theorem LinearMap.injective_of_forall_localization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsNoetherianRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (map : M →ₗ[R] N) (local_injective : ∀ (prime : Ideal R) [inst : prime.IsPrime], Function.Injective ⇑((LocalizedModule.map prime.primeCompl) map) ∨ prime ∉ associatedPrimes R M) : Function.Injective ⇑map

A linear map is injective if its localization is injective at every associated prime of its domain. This is Stacks 0AV7 for the canonical localization modules.