isClosed_singleton_iff_locallyOfFiniteType

English

If f: X → Y is a morphism and s ⊆ Y is constructible, then its preimage f^{-1}(s) is constructible.

Русский

Если f: X → Y и s ⊆ Y конструктивна, то её предобраз по f конструктивен.

LaTeX

$$$\forall f, \ f\text{ is morphism},\ IsConstructible(s) \Rightarrow \ IsConstructible(f^{-1}(s)).$$$

Lean4

@[stacks 01TB "(1) => (2)"]
theorem isClosed_singleton_iff_locallyOfFiniteType {X : Scheme.{u}} [JacobsonSpace X] {x : X} :
    IsClosed ({ x } : Set X) ↔ LocallyOfFiniteType (X.fromSpecResidueField x) :=
  by
  constructor
  ·
    exact fun H ↦
      have := isClosed_singleton_iff_isClosedImmersion.mp H;
      inferInstance
  · intro H
    simpa using
      (X.fromSpecResidueField x).closePoints_subset_preimage_closedPoints (IsLocalRing.isClosed_singleton_closedPoint _)

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