Localizations of modules at the complement of a prime ideal

@[reducible, inline]

abbrev IsLocalizedModule.AtPrime {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] (P : Ideal R) [P.IsPrime] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') : Prop

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.

Equations

• IsLocalizedModule.AtPrime P f = IsLocalizedModule P.primeCompl f

@[reducible, inline]

abbrev LocalizedModule.AtPrime {R : Type u_1} [CommSemiring R] (P : Ideal R) [P.IsPrime] (M : Type u_2) [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

Given a prime ideal P, LocalizedModule.AtPrime P M is a localization of M at the complement of P.

Equations

• LocalizedModule.AtPrime P M = LocalizedModule P.primeCompl M