English
Let P be a prime ideal of a commutative semiring R, and f: M →ₗ[R] M' a linear map of modules. Then IsLocalizedModule.AtPrime P f describes that M' is isomorphic to the localization of M at the complement of P.
Русский
Пусть P — простой идеал кольца R, и f: M →ₗ[R] M' — линейный отображение модулей. Тогда IsLocalizedModule.AtPrime P f описывает, что M' изоморфен локализации M по дополнению к P.
LaTeX
$$$M' \\cong_R S^{-1}M$ where $S = R \\setminus P$.$$
Lean4
/-- Given a prime ideal `P` and `f : M →ₗ[R] M'`, `IsLocalizedModule.AtPrime P f` states that `M'`
is isomorphic to the localization of `M` at the complement of `P`. -/
protected abbrev AtPrime {R M M' : Type*} [CommSemiring R] (P : Ideal R) [P.IsPrime] [AddCommMonoid M]
[AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') :=
IsLocalizedModule P.primeCompl f
