English
If P has HasAffineProperty with respect to an affine-and-Q construction, and certain base-change and descent conditions hold, then P descends along quasi-compact morphisms.
Русский
Если P имеет свойство HasAffineProperty относительно аффинного конструирования и Q, а также выполняются условия базового изменения и десцентности, тогда P спускается вдоль квазик compacto отображений.
LaTeX
$$$[HasAffineProperty\\ P\\ (affineAnd\\ Q)] \\Rightarrow \\text{DescendsAlong}(P' \\wedge QuasiCompact)$ under the given base-change and Q-codescends assumptions$$
Lean4
/-- 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.
-/
nonrec theorem descendsAlong_of_affineAnd (hP : HasAffineProperty P (affineAnd Q))
[MorphismProperty.DescendsAlong (@IsAffineHom) P'] (hQ : RingHom.RespectsIso Q)
(hQQ' : RingHom.CodescendsAlong Q Q') : P.DescendsAlong (P' ⊓ @QuasiCompact) :=
by
apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ H₁
introv h hf
have : IsAffine Y := by
convert isAffine_of_isAffineHom g
exact
MorphismProperty.of_pullback_fst_of_descendsAlong h <|
AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom P inferInstance _ hf
wlog hY : ∃ S, Y = Spec S generalizing Y
· rw [← P.cancel_left_of_respectsIso Y.isoSpec.inv]
have heq :
pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
pullback.map _ _ _ _ (𝟙 _) (Y.isoSpec.inv) (𝟙 _) (by simp) (by simp) ≫ pullback.fst (Spec.map φ) g :=
(pullback.lift_fst _ _ _).symm
refine this _ ?_ inferInstance ⟨_, rfl⟩
rwa [heq, P.cancel_left_of_respectsIso]
obtain ⟨Y, rfl⟩ := hY
apply of_pullback_fst_Spec_of_codescendsAlong _ _ hQQ' H₂ _ h hf
simp [SpecMap_iff_of_affineAnd _ hQ]
