Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X]
  [AlgebraicGeometry.IsZariskiLocalAtSource P] [P.ContainsIdentities],
  ∃ Y p, AlgebraicGeometry.Surjective p ∧ P p ∧ AlgebraicGeometry.IsAffine Y

If P is local at the source, every quasi-compact scheme is dominated by an affine scheme via p : Y ⟶ X such that p satisfies P.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Descent

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompactSpaceAlgebraicGeometry.IsZariskiLocalAtSourceCategoryTheory.MorphismProperty.ContainsIdentities