AlgebraicGeometry.reduce_to_affine_global

theorem AlgebraicGeometry.reduce_to_affine_global : ∀ (P : (X : AlgebraicGeometry.Scheme) → TopologicalSpace.Opens ↑↑X.toPresheafedSpace → Prop), (∀ (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P X V) → P X U) → (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.IsOpenImmersion f], ∃ U V, ∃ (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P X { carrier := U, is_open' := ⋯ } → P Y { carrier := V, is_open' := ⋯ }) → (∀ (R : CommRingCat), P (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) ⊤) → ∀ (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), P X U

This theorem, `AlgebraicGeometry.reduce_to_affine_global`, states a strategy for proving a property `P` holds for all open subsets of all algebraic schemes. The theorem outlines three conditions that, if satisfied, ensure the property `P` holds universally: 1. Locality: In any scheme `X`, if `P` holds for an open cover of a subset `U`, then `P` holds for `U` itself. 2. Stability under open immersions: For an open immersion (a morphism that respects the locally ringed space structure) `f` from scheme `X` to `Y`, if `P` holds for the entire space of `X`, then `P` also holds for the image of `f` in `Y`. 3. Affine case: `P` holds for the entire space of an affine scheme. An affine scheme is the spectrum of a commutative ring, seen as a contravariant functor from commutative rings to schemes. If these conditions are met, the theorem concludes that `P` holds for all open subsets of all algebraic schemes.

More concisely: Given a property `P` satisfying locality, stability under open immersions, and holding for affine schemes, `P` universally holds for all open subsets of all algebraic schemes.