Theorems · Definition · commutative algebra
PrimeSpectrum.toPiLocalization
(R : Type u_1) → [inst : CommSemiring R] → R →ₐ[R] PrimeSpectrum.PiLocalization R
The canonical ring homomorphism from a commutative semiring to the product of its localizations at all prime ideals. It is always injective.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- AlgHomstatement · cited by 3,236
- PrimeSpectrumstatement · cited by 625
- Ideal.primeComplstatement · cited by 462
- PrimeSpectrum.asIdealstatement · cited by 333
- Localizationstatement · cited by 270
- Algebra.ofIdproof · cited by 166
- PrimeSpectrum.PiLocalizationstatement and proof · cited by 20
Cited by14
Results whose statement or proof uses this declaration.
- PrimeSpectrum.toPiLocalizationEquivproof · cited by 3
- PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalizationstatement · cited by 2
- PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijectivestatement · cited by 2
- PrimeSpectrum.toPiLocalization_injectivestatement and proof · cited by 2
- PrimeSpectrum.toPiLocalization_surjective_of_discreteTopologystatement · cited by 2
- PrimeSpectrum.finite_of_toPiLocalization_pi_surjectivestatement and proof · cited by 1
- PrimeSpectrum.finite_of_toPiLocalization_surjectivestatement and proof · cited by 1
- IsArtinianRing.exists_not_mem_forall_mem_of_neproof · cited by 1
- PrimeSpectrum.isMaximal_of_toPiLocalization_surjectivestatement and proof · cited by 1
- PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjectivestatement · cited by 1
- PrimeSpectrum.discreteTopology_of_toLocalization_surjectivestatement and proof · cited by 1
- PrimeSpectrum.mapPiLocalization_naturalitystatement · cited by 1