Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong

∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [P'.IsStableUnderBaseChange],
  (∀ {R : CommRingCat} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec R)
      (g : Y ⟶ AlgebraicGeometry.Spec R), P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g) →
    P.DescendsAlong P'

If P is local at the target, to show P descends along P' we may assume the base to be affine.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Descent

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsZariskiLocalAtTargetCategoryTheory.MorphismProperty.IsStableUnderBaseChange