Theorems · Definition · commutative algebra
MaximalSpectrum.toPiLocalization
(R : Type u_1) → [inst : CommSemiring R] → R →ₐ[R] MaximalSpectrum.PiLocalization R
The canonical ring homomorphism from a commutative semiring to the product of its localizations at all maximal ideals. It is always injective.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, 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
- Ideal.primeComplstatement · cited by 462
- Localization.AtPrimestatement · cited by 299
- Algebra.ofIdproof · cited by 166
- MaximalSpectrumstatement · cited by 73
- MaximalSpectrum.asIdealstatement · cited by 58
- MaximalSpectrum.PiLocalizationstatement and proof · cited by 17
Cited by10
Results whose statement or proof uses this declaration.
- MaximalSpectrum.toPiLocalization_injectivestatement and proof · cited by 3
- PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalizationstatement · cited by 2
- MaximalSpectrum.toPiLocalizationEquivproof · cited by 2
- MaximalSpectrum.toPiLocalization_not_surjective_of_infinitestatement and proof · cited by 2
- MaximalSpectrum.finite_of_toPiLocalization_pi_surjectivestatement and proof · cited by 1
- PrimeSpectrum.toPiLocalization_not_surjective_of_infiniteproof · cited by 1
- MaximalSpectrum.mapPiLocalization_naturalitystatement · cited by 1
- MaximalSpectrum.toPiLocalization_apply_applystatement · cited by 0
- PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopologystatement · cited by 0
- MaximalSpectrum.finite_of_toPiLocalization_surjectivestatement and proof · cited by 0