English
If P is Zariski-local at the target and P', IsStableUnderBaseChange and IsStableUnderComposition hold, then P descends along the infimum with QuasiCompact.
Русский
Если P локален по Зарику к цели, и P' стабилен по базовым изменениям и по композициям, то P спускается вдоль инфимума с квази-Компактностью.
LaTeX
$$$[IsZariskiLocalAtTarget P] [P'.IsStableUnderBaseChange] [P'.IsStableUnderComposition] (H : \\forall R X Y f g, P'(f) \\to P( pullback.fst f g) \\to P g) : P.DescendsAlong (P' \\wedge @QuasiCompact)$$$
Lean4
theorem descendsAlong_inf_quasiCompact [IsZariskiLocalAtTarget P]
(H :
∀ {R S : CommRingCat.{u}} {Y : Scheme.{u}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g) :
P.DescendsAlong (P' ⊓ @QuasiCompact) :=
by
apply IsZariskiLocalAtTarget.descendsAlong
intro R X Y f g hf h
wlog hX : ∃ T, X = Spec T generalizing X
· have _ : CompactSpace X := by simpa [← quasiCompact_over_affine_iff f] using hf.2
obtain ⟨Y, p, hsurj, hP', hY⟩ := X.exists_hom_isAffine_of_isZariskiLocalAtSource @IsLocalIso
refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩
· rw [Category.assoc, (P' ⊓ @QuasiCompact).cancel_left_of_respectsIso]
exact ⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩
· rw [← pullbackRightPullbackFstIso_inv_fst f g _, P.cancel_left_of_respectsIso]
exact P.pullback_fst _ _ h
obtain ⟨T, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
exact H φ g hf.1 h
