Theorems · Theorem · commutative algebra

Localization.existsUnique_algebraMap_eq_of_span_eq_top

∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : (a : ↑s) → Localization.Away ↑a),
      (∀ (a b : ↑s),
          (IsLocalization.Away.awayToAwayRight ↑a ↑b) (f a) = (IsLocalization.Away.awayToAwayLeft ↑b ↑a) (f b)) →
        ∃! r, ∀ (a : ↑s), (algebraMap R (Localization.Away ↑a)) r = f a

The sheaf condition for the structure sheaf on Spec R for a covering of the whole prime spectrum by basic opens.

Defined in

Mathlib.RingTheory.Localization.Away.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiring