Theorems · Theorem · commutative algebra

IsLocalization.Away.of_surjective

∀ {S : Type u_4} {T : Type u_5} [inst : CommRing S] [inst_1 : CommRing T] [inst_2 : Algebra S T],
  Function.Surjective ⇑(algebraMap S T) →
    ∀ {r : S},
      IsUnit ((algebraMap S T) r) → ∀ (n : ℕ), r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥ → IsLocalization.Away r T

Suppose I is an ideal of R, then R / I is the localization away from r : R if r - 1 ∈ I and for some n, r ^ n • I = ⊥. For sake of usability, we state this for surjective ring maps instead of ideals. For a version with two ideals, see Away.of_sub_one_mem_ker'.

Defined in

Mathlib.RingTheory.Localization.Away.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra