Theorems · Definition · commutative algebra

PrimeSpectrum.mapPiLocalization

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] → (R →+* S) → PrimeSpectrum.PiLocalization R →+* PrimeSpectrum.PiLocalization S

A ring homomorphism induces a homomorphism between the products of localizations at primes.

Defined in: Mathlib.RingTheory.Spectrum.Maximal.Localization
Cited by: 5 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommSemiringstatement and proof · cited by 10,911
RingHomstatement and proof · cited by 10,189
RingHom.compproof · cited by 899
PrimeSpectrumstatement and proof · cited by 625
Ideal.primeComplstatement and proof · cited by 462
Ideal.comapproof · cited by 443
PrimeSpectrum.asIdealstatement and proof · cited by 333
Localizationstatement and proof · cited by 270
PrimeSpectrum.comapproof · cited by 199
Localization.localRingHomproof · cited by 54
Pi.evalRingHomproof · cited by 44
RingHom.piproof · cited by 26

Cited by5

Results whose statement or proof uses this declaration.

PrimeSpectrum.finite_of_toPiLocalization_surjectiveproof · cited by 1
PrimeSpectrum.mapPiLocalization_bijectivestatement and proof · cited by 1
PrimeSpectrum.mapPiLocalization_compstatement · cited by 1
PrimeSpectrum.mapPiLocalization_idstatement · cited by 1
PrimeSpectrum.mapPiLocalization_naturalitystatement · cited by 1