Theorems · Theorem · commutative algebra

IsLocalization.surjective_quotientMap_of_maximal_of_localization

∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] {I : Ideal S} [I.IsPrime] {J : Ideal R} {H : J ≤ Ideal.under R I},
  (Ideal.under R I).IsMaximal → Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)

quotientMap applied to maximal ideals of a localization is surjective. The quotient by a maximal ideal is a field, so inverses to elements already exist, and the localization necessarily maps the equivalence class of the inverse in the localization

Defined in: Mathlib.RingTheory.Localization.Ideal
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra IsLocalization Ideal.IsPrime

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites36

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
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Top.topproof · cited by 9,680
Idealstatement and proof · cited by 4,748
Algebra.algebraMapstatement and proof · cited by 4,706
Submonoidstatement and proof · cited by 3,086
HasQuotient.Quotientstatement and proof · cited by 2,301
map_zeroproof · cited by 1,614
le_rflproof · cited by 1,558
map_mulproof · cited by 1,137

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.jacobson_bot_of_integral_localizationproof · cited by 0