API for localized modules away from an element

We provide some specialized API for the localization of a module away from an element.

theorem IsLocalizedModule.Away.mk {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} {r : R} (h₁ : IsUnit ((algebraMap R (Module.End R N)) r)) (h₂ : ∀ (x : N), ∃ (n : ℕ) (y : M), r ^ n • x = f y) (h₃ : ∀ (x y : M), f x = f y → ∃ (n : ℕ), r ^ n • x = r ^ n • y) : IsLocalizedModule.Away r f

theorem IsLocalizedModule.Away.mk_of_addCommGroup {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {f : M →ₗ[R] N} {r : R} (h₁ : IsUnit ((algebraMap R (Module.End R N)) r)) (h₂ : ∀ (x : N), ∃ (n : ℕ) (y : M), r ^ n • x = f y) (h₃ : ∀ (x : M), f x = 0 → ∃ (n : ℕ), r ^ n • x = 0) : IsLocalizedModule.Away r f

theorem IsLocalizedModule.Away.isUnit_algebraMap {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (r : R) [IsLocalizedModule.Away r f] : IsUnit ((algebraMap R (Module.End R N)) r)

theorem IsLocalizedModule.Away.exists_of_eq {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} (r : R) [IsLocalizedModule.Away r f] {x y : M} (h : f x = f y) : ∃ (n : ℕ), r ^ n • x = r ^ n • y

theorem IsLocalizedModule.Away.surj {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (r : R) [IsLocalizedModule.Away r f] (y : N) : ∃ (n : ℕ) (x : M), r ^ n • y = f x

theorem IsLocalizedModule.Away.of_associated {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} {r r' : R} (h : Associated r r') [IsLocalizedModule.Away r f] : IsLocalizedModule.Away r' f

theorem IsLocalizedModule.Away.iff_of_associated {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} {r r' : R} (h : Associated r r') : IsLocalizedModule.Away r f ↔ IsLocalizedModule.Away r' f