English
A refinement of the previous quasi-compactness result in a specific construction; in particular, certain basis choices yield compactness conclusions for pullbacks under universal closedness assumptions.
Русский
Уточнение к предыдущему результату о квази-замкнутости в конкретной конструкции; в частности, выбор базиса даёт вывод о компактности для произведений по основанию при предпосылке универсально замкнутости.
LaTeX
$$$$\text{(variant of compactness under universal closedness).}$$$$
Lean4
@[stacks 04XU]
theorem isProperMap (f : X.Hom Y) [UniversallyClosed f] : IsProperMap f.base :=
by
rw [isProperMap_iff_isClosedMap_and_compact_fibers]
refine ⟨Scheme.Hom.continuous f, ?_, ?_⟩
· exact MorphismProperty.universally_le (P := topologically @IsClosedMap) _ UniversallyClosed.out
· intro y
have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))
rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]
exact isCompact_range (Scheme.Hom.continuous _)
