Theorems · Definition · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme

(X : AlgebraicGeometry.LocallyRingedSpace) →
  (∀ (x : ↑X.toTopCat),
      ∃ R f,
        x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ∧
          AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f) →
    AlgebraicGeometry.Scheme

To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

0 results in Mathlib

Foundations

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