closePoints_subset_preimage_closedPoints

English

Same Jacobson-space special case: finite iff locally of finite type.

Русский

Повторение случая Якобсона: конечность эквивалентна локальному конечному типу.

LaTeX

$$$\mathrm{IsFinite}(f) \iff \mathrm{LocallyOfFiniteType}(f).$$$

Lean4

@[stacks 01TB "(1) => (3)"]
theorem closePoints_subset_preimage_closedPoints {X Y : Scheme.{u}} (f : X ⟶ Y) [JacobsonSpace Y]
    [LocallyOfFiniteType f] : closedPoints X ⊆ f.base ⁻¹' closedPoints Y :=
  by
  intro x hx
  have := isClosed_singleton_iff_isClosedImmersion.mp hx
  have := (isFinite_iff_locallyOfFiniteType_of_jacobsonSpace (f := X.fromSpecResidueField x ≫ f)).mpr inferInstance
  simpa [Set.range_comp, Scheme.range_fromSpecResidueField] using
    (X.fromSpecResidueField x ≫ f).isClosedMap.isClosed_range

Похожие утверждения