Theorems · Theorem · commutative algebra
Localization.AtPrime.map_eq_maximalIdeal
∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)The image of I in the localization at I.primeCompl is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure AtPrime.isLocalRing
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringIdeal.IsPrime
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 · cited by 10,189
- Idealstatement and proof · cited by 4,748
- Algebra.algebraMapstatement and proof · cited by 4,706
- Ideal.IsPrimestatement and proof · cited by 827
- Ideal.mapstatement and proof · cited by 692
- Ideal.primeComplstatement and proof · cited by 462
- Localization.AtPrimestatement and proof · cited by 299
- IsLocalRing.maximalIdealstatement and proof · cited by 297
- Localizationstatement and proof · cited by 270
- Ideal.underproof · cited by 170
- IsLocalization.map_underproof · cited by 12
Cited by17
Results whose statement or proof uses this declaration.
- Ideal.ramificationIdx_posproof · cited by 5
- Ideal.ramificationIdx_eq_one_iffproof · cited by 4
- Ideal.ramificationIdx_eq_oneproof · cited by 3
- Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iffproof · cited by 3
- Ideal.ramificationIdx'_eq_one_of_map_localizationproof · cited by 3
- Ideal.ramificationIdx'_eq_ramificationIdx'proof · cited by 3
- Ideal.ramificationIdx_tower'proof · cited by 2
- Algebra.isUnramifiedAt_iff_map_eqproof · cited by 2
- IsUnramifiedAt.of_liesOver_of_ne_botproof · cited by 1
- isStronglyTranscendental_mk_of_mem_minimalPrimesproof · cited by 1
- Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRingproof · cited by 1
- Module.support_quotientproof · cited by 1