Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact

∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P'.IsStableUnderBaseChange]
  [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange],
  @AlgebraicGeometry.IsLocalIso ⊓ @AlgebraicGeometry.Surjective ≤ P' →
    ∀ [AlgebraicGeometry.IsZariskiLocalAtTarget P],
      (∀ {R S : CommRingCat} {Y : AlgebraicGeometry.Scheme} (φ : R ⟶ S) (g : Y ⟶ AlgebraicGeometry.Spec R),
          P' (AlgebraicGeometry.Spec.map φ) →
            P (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map φ) g) → P g) →
        P.DescendsAlong (P' ⊓ @AlgebraicGeometry.QuasiCompact)

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Descent

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.IsZariskiLocalAtTarget