Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen

∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  Ideal.span s = ⊤ → (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) → AlgebraicGeometry.IsAffineOpen U

If s is a spanning set of Γ(X, U), such that each X.basicOpen i is affine, then U is also affine.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Affine

Cited by

0 results in Mathlib

Foundations

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