Theorems · Theorem · commutative algebra

Polynomial.jacobson_bot_of_integral_localization

∀ {S : Type u_2} [inst : CommRing S] [IsDomain S] {R : Type u_5} [inst_2 : CommRing R] [IsDomain R] [IsJacobsonRing R]
  (Rₘ : Type u_6) (Sₘ : Type u_7) [inst_5 : CommRing Rₘ] [inst_6 : CommRing Sₘ] (φ : R →+* S),
  Function.Injective ⇑φ →
    ∀ (x : R),
      x ≠ 0 →
        ∀ [inst_7 : Algebra R Rₘ] [inst_8 : IsLocalization.Away x Rₘ] [inst_9 : Algebra S Sₘ]
          [inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ],
          (IsLocalization.map Sₘ φ ⋯).IsIntegral → ⊥.jacobson = ⊥

If f : R → S descends to an integral map in the localization at x, and R is a Jacobson ring, then the intersection of all maximal ideals in S is trivial

Defined in

Mathlib.RingTheory.Jacobson.Ring

Cited by

0 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainCommRingIsDomainIsJacobsonRingCommRingCommRingAlgebraIsLocalization.AwayAlgebraIsLocalization