Bijectivity from local depth conditions

A linear map is bijective if, at every prime, either its localization is bijective, or the localized source has depth at least two and the prime is not associated to the target. This criterion applies to arbitrary source and target modules over a Noetherian ring.

References

• Stacks Project, Lemma 15.24.12 (Tag 0AV7), for the injectivity criterion.
• Stacks Project, Lemma 15.24.13 (Tag 0AV8).

theorem LinearMap.bijective_of_depth_of_addCommGroup {R : Type u} {M : Type v} {N : Type w} [CommRing R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (map : M →ₗ[R] N) (hypothesis : ∀ (prime : Ideal R) [inst : prime.IsPrime], Function.Bijective ⇑((LocalizedModule.map prime.primeCompl) map) ∨ 2 ≤ IsLocalRing.depth ↧(LocalizedModule prime.primeCompl M) ∧ prime ∉ associatedPrimes R N) : Function.Bijective ⇑map

A linear map between arbitrary additive-group modules over a Noetherian ring is bijective if, at each prime, its localization is bijective or the localized source M_p has depth at least two over R_p and the prime is not associated to the target. The additive-group structures are arbitrary; LinearMap.bijective_of_depth is the version for the canonical group structure.

Divergence from Stacks: no finite-source hypothesis is needed here.

theorem LinearMap.bijective_of_depth {R : Type u} {M : Type v} {N : Type w} [CommRing R] [IsNoetherianRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (map : M →ₗ[R] N) (hypothesis : ∀ (prime : Ideal R) [inst : prime.IsPrime], Function.Bijective ⇑((LocalizedModule.map prime.primeCompl) map) ∨ 2 ≤ IsLocalRing.depth ↧(LocalizedModule prime.primeCompl M) ∧ prime ∉ associatedPrimes R N) : Function.Bijective ⇑map

A linear map between arbitrary modules over a Noetherian ring is bijective if, at each prime, its localization is bijective or the localized source M_p has depth at least two over R_p and the prime is not associated to the target. The depth hypothesis uses the canonical additive group structure induced by the ring action; see LinearMap.bijective_of_depth_of_addCommGroup for arbitrary additive-group structures.

Divergence from Stacks: no finite-source hypothesis is needed here.