Theorems · Definition · commutative algebra
Localization.awayMap
{R : Type u_1} →
[inst : CommSemiring R] →
{P : Type u_3} →
[inst_1 : CommSemiring P] → (f : R →+* P) → (r : R) → Localization.Away r →+* Localization.Away (f r)Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 64 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.
Cites6
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
- Submonoid.powersstatement · cited by 408
- Localization.Awaystatement and proof · cited by 162
- IsLocalization.Away.mapproof · cited by 19
Cited by37
Results whose statement or proof uses this declaration.
- RingHom.OfLocalizationSpanproof · cited by 16
- Algebra.ZariskisMainPropertyproof · cited by 10
- RingHom.OfLocalizationSpanTarget.ofLocalizationSpanproof · cited by 7
- Localization.awayMap_surjective_iffstatement · cited by 4
- Algebra.zariskisMainProperty_iffproof · cited by 3
- Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijectivestatement and proof · cited by 3
- RingHom.RespectsIso.isLocalization_away_iffstatement · cited by 2
- RingHom.OfLocalizationSpan.andproof · cited by 1
- RingHom.OfLocalizationSpan.mkproof · cited by 1
- RingHom.OfLocalizationSpan.ofIsLocalizationproof · cited by 1