Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd

∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  (Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) [P'.IsStableUnderBaseChange]
  [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange],
  @AlgebraicGeometry.IsLocalIso ⊓ @AlgebraicGeometry.Surjective ≤ P' →
    (∀ {R S : CommRingCat} {f : R ⟶ S}, P' (AlgebraicGeometry.Spec.map f) → Q' (CommRingCat.Hom.hom f)) →
      AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ [CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.IsAffineHom) P'],
          (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
            (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] =>
                Q') →
              P.DescendsAlong (P' ⊓ @AlgebraicGeometry.QuasiCompact)

Let P be a morphism property associated with affineAnd Q. Suppose - P' implies Q' on global sections on affine schemes, - P' is satisfied for surjective, local isomorphisms, - affine morphisms descend along P'', and - Q codescends along Q', Then P descends along quasi-compact morphisms satisfying P'. Note: The second condition is in particular satisfied for faithfully flat morphisms.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Descent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.DescendsAlong