Theorems · Definition · commutative algebra
MaximalSpectrum.mapPiLocalization
{R : Type u_1} →
{S : Type u_2} →
[inst : CommSemiring R] →
[inst_1 : CommSemiring S] →
(f : R →+* S) → Function.Bijective ⇑f → MaximalSpectrum.PiLocalization R →+* MaximalSpectrum.PiLocalization SFunctoriality of PiLocalization but restricted to bijective ring homs.
If R and S are commutative rings, surjectivity would be enough.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement and proof · cited by 10,189
- RingHom.compproof · cited by 899
- Function.Bijectivestatement and proof · cited by 863
- Ideal.primeComplstatement · cited by 462
- Ideal.comapproof · cited by 443
- Localization.AtPrimestatement and proof · cited by 299
- MaximalSpectrumstatement and proof · cited by 73
- MaximalSpectrum.asIdealstatement and proof · cited by 58
- Localization.localRingHomproof · cited by 54
- Pi.evalRingHomproof · cited by 44
Cited by6
Results whose statement or proof uses this declaration.
- MaximalSpectrum.mapPiLocalization_idstatement · cited by 1
- MaximalSpectrum.mapPiLocalization_bijectivestatement and proof · cited by 1
- MaximalSpectrum.mapPiLocalization_compstatement · cited by 1
- MaximalSpectrum.mapPiLocalization.congr_simpstatement and proof · cited by 1
- MaximalSpectrum.mapPiLocalization_naturalitystatement · cited by 1
- MaximalSpectrum.finite_of_toPiLocalization_surjectiveproof · cited by 0