Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact

∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens},
  IsCompact U.carrier →
    ∀ (x f : ↑(X.presheaf.obj (Opposite.op U))),
      TopCat.Presheaf.restrictOpen x (X.basicOpen f) ⋯ = 0 → ∃ n, f ^ n * x = 0

If x : Γ(X, U) is zero on D(f) for some f : Γ(X, U), and U is quasi-compact, then f ^ n * x = 0 for some n.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Cited by

3 results in Mathlib

Foundations

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