Localizations of modules away from an element #
@[reducible, inline]
abbrev
IsLocalizedModule.Away
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommSemiring R]
(x : R)
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M']
[Module R M']
(f : M →ₗ[R] M')
:
Given x : R and f : M →ₗ[R] M', IsLocalization.Away x fstates thatM'is isomorphic to the localization ofMat the submonoid generated byx`.
Equations
Instances For
@[reducible, inline]
abbrev
LocalizedModule.Away
{R : Type u_1}
[CommSemiring R]
(x : R)
(M : Type u_2)
[AddCommMonoid M]
[Module R M]
:
Type (max u_1 u_2)
Given x : R, LocalizedModule.Away x M is the localization of M at the
submonoid generated by x.
Equations
- LocalizedModule.Away x M = LocalizedModule (Submonoid.powers x) M