Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasRingHomProperty.descendsAlong

∀ (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.HasRingHomProperty P 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 the morphism property associated to the ring hom property Q. Suppose - P' implies Q' on global sections for affine schemes, - P' is satisfied for all surjective, local isomorphisms, and - Q codescend 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

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.HasRingHomProperty