theorem
QCohTildeFunctor.element_zero_of_localization_zero
{R : Type u_1}
[CommRing R]
{N : Type u_2}
[AddCommGroup N]
[Module R N]
(n : N)
(h : ∀ (P : Ideal R) [inst : P.IsMaximal], (LocalizedModule.mkLinearMap P.primeCompl N) n = 0)
:
An element of a module is zero whenever its image in every maximal localization vanishes; the standard local-to-global zero criterion.
theorem
QCohTildeFunctor.localization_localization_isLocalization'
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsLocalization M S]
(N : Submonoid S)
(T : Type u_3)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
[IsLocalization N T]
:
Iterated localization T = N^{-1}(M^{-1} R) realizes T as a localization
of R at a single combined submonoid, the transitivity-of-localization principle.