Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isLocalization_basicOpen_of_qcqs

∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))

If U is qcqs, then Γ(X, D(f)) ≃ Γ(X, U)_f for every f : Γ(X, U). This is known as the Qcqs lemma in [R. Vakil, The rising sea][RisingSea].

Defined in

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Cited by

3 results in Mathlib

Foundations

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