Theorems · Theorem · algebraic geometry

AlgebraicGeometry.reduce_to_affine_global

∀ (P : {X : AlgebraicGeometry.Scheme} → X.Opens → Prop) {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  (∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U) →
    (∀ (X Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
        ∃ U V, U = ⊤ ∧ V = AlgebraicGeometry.Scheme.Hom.opensRange f ∧ (P U → P V)) →
      (∀ (R : CommRingCat), P ⊤) → P U

To show that a statement P holds for all open subsets of all schemes, it suffices to show that 1. In any scheme X, if P holds for an open cover of U, then P holds for U. 2. For an open immersion f : X ⟶ Y, if P holds for the entire space of X, then P holds for the image of f. 3. P holds for the entire space of an affine scheme.

Defined in

Mathlib.AlgebraicGeometry.Properties

Cited by

1 results in Mathlib

Foundations

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