English
The first and second projections in a pullback of schemes along any morphisms are quasi-compact when one of the legs is quasi-compact.
Русский
Первая и вторая проекции в пуш-бэке схем по любым морфизмам квази-компактны, когда одна из ножек квази-компактна.
LaTeX
$$$\\text{QuasiCompact}(\\mathrm{pullback.fst})$ and $\\text{QuasiCompact}(\\mathrm{pullback.snd})$ under assumptions$$
Lean4
/-- A section over a compact open of a scheme is nilpotent if and only if its associated
basic open is empty. -/
theorem isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : Scheme.{u}} {U : X.Opens} (hU : IsCompact (U : Set X))
(f : Γ(X, U)) : IsNilpotent f ↔ X.basicOpen f = ⊥ :=
by
refine ⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩
have h : (1 : Γ(X, U)) |_ (X.basicOpen f) = 0 :=
by
have e : X.basicOpen f ≤ ⊥ := by rw [hf]
rw [← TopCat.Presheaf.restrict_restrict e bot_le]
rw [Subsingleton.eq_zero (1 |_ ⊥)]
change X.presheaf.map _ 0 = 0
rw [map_zero]
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h
rw [mul_one] at hn
use n
