Descent of morphism properties

Let P and P' be morphism properties. In this file we show some results to deduce that P descends along P' from a codescent property of ring homomorphisms.

Main results

• HasRingHomProperty.descendsAlong: if P is a local property induced by Q, P' implies Q' on global sections of affines and Q codescends along Q', then P descends along P'.
• HasAffineProperty.descendsAlong_of_affineAnd: if P is given by affineAnd Q, P' implies Q' on global sections of affines and Q codescends along Q', then P descends along P' (see TODOs).

TODO

• Show that affine morphisms descend along faithfully-flat morphisms. This will make HasAffineProperty.descendsAlong_of_affineAnd useful.

theorem AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) (X : Scheme) [CompactSpace ↥X] [IsLocalAtSource P] [P.ContainsIdentities] : ∃ (Y : Scheme) (p : Y ⟶ X), Surjective p ∧ P p ∧ 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.

theorem AlgebraicGeometry.IsLocalAtTarget.descendsAlong (P P' : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] [P'.IsStableUnderBaseChange] (H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ 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.

theorem AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong (P P' : CategoryTheory.MorphismProperty Scheme) {Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [P.RespectsIso] (hQQ' : RingHom.CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => Q) fun {R S : Type u} [CommRing R] [CommRing S] => Q') (H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)) (H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)) {R S T : CommRingCat} {f : Spec T ⟶ Spec R} {g : Spec S ⟶ Spec R} (h : P' f) (hf : P (CategoryTheory.Limits.pullback.fst f g)) : P g

theorem AlgebraicGeometry.IsStableUnderBaseChange.of_pullback_fst_of_isAffine (P P' : CategoryTheory.MorphismProperty Scheme) [P'.RespectsIso] [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange] (H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (CategoryTheory.Limits.pullback.fst f g) → P g) {X Y Z T : Scheme} [IsAffine T] (p : T ⟶ X) (hp : P' p) (f : X ⟶ Z) (g : Y ⟶ Z) (h : P' f) (hf : P (CategoryTheory.Limits.pullback.fst f g)) : P g

If X admits a morphism p : T ⟶ X from an affine scheme satisfying P', to show a property descends along a morphism f : X ⟶ ZsatisfyingP', X` may assumed to be affine.

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

theorem AlgebraicGeometry.HasRingHomProperty.descendsAlong (P P' : CategoryTheory.MorphismProperty Scheme) (Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) [P'.IsStableUnderBaseChange] [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange] (H₁ : @IsLocalIso ⊓ @Surjective ≤ P') (H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)) [HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] => Q] (hQQ' : RingHom.CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => Q) fun {R S : Type u} [CommRing R] [CommRing S] => Q') : P.DescendsAlong (P' ⊓ @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 satisfiying P'.

Note: The second condition is in particular satisfied for faithfully flat morphisms.

theorem AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd (P P' : CategoryTheory.MorphismProperty Scheme) (Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) [P'.IsStableUnderBaseChange] [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange] (H₁ : @IsLocalIso ⊓ @Surjective ≤ P') (H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)) (hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] => Q)) [CategoryTheory.MorphismProperty.DescendsAlong (@IsAffineHom) P'] (hQ : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hQQ' : RingHom.CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => Q) fun {R S : Type u} [CommRing R] [CommRing S] => Q') : P.DescendsAlong (P' ⊓ @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.