English
If P is Zariski-local at the target, and P', together with base-change is stable under infimum operations, then P descends along the infimum of P' and quasi-compactness.
Русский
Если P локален по Зарискирскому очку к цели, и P' вместе с устойчивостью по основанию сохраняют инфимную структуру, то P спускается вдоль инфимума P' и квази-однородности.
LaTeX
$$$[IsZariskiLocalAtTarget\\ P] \\Rightarrow P.DescendsAlong (P' \\wedge QuasiCompact)$$$
Lean4
/-- If `X` admits a morphism `p : T ⟶ X` from an affine scheme satisfying `P', to
show a property descends along a morphism `f : X ⟶ Z` satisfying `P'`, `X` may assumed to
be affine. -/
theorem of_pullback_fst_of_isAffine [P'.RespectsIso] [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange]
(H : ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g)
{X Y Z T : Scheme.{u}} [IsAffine T] (p : T ⟶ X) (hp : P' p) (f : X ⟶ Z) (g : Y ⟶ Z) (h : P' f)
(hf : P (pullback.fst f g)) : P g := by
apply H ((T.isoSpec.inv ≫ p) ≫ f)
· rw [Category.assoc, P'.cancel_left_of_respectsIso]
exact P'.comp_mem _ _ hp h
· rw [← pullbackRightPullbackFstIso_inv_fst f g (T.isoSpec.inv ≫ p), P.cancel_left_of_respectsIso]
exact P.pullback_fst _ _ hf
