theorem injective_of_localization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Injective ⇑((map' J.primeCompl) f)) : Function.Injective ⇑f

theorem surjective_of_localization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Surjective ⇑((map' J.primeCompl) f)) : Function.Surjective ⇑f

theorem bijective_of_localization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f)) : Function.Bijective ⇑f

noncomputable def linearEquivOfLocalization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f)) : M ≃ₗ[R] N

Equations

• linearEquivOfLocalization f h = LinearEquiv.ofBijective f ⋯

theorem linearEquivOfLocalization_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f)) (m : M) : (linearEquivOfLocalization f h) m = f m