isConstructible_image — Mathlib

English

Under a morphism of finite presentation into a qcqs scheme, the image of a constructible set is constructible.

Русский

При отображении конечной презентации в qcqs-множество образ конструктивной множества — конструктивен.

LaTeX

$$$\text{IsConstructible}(f.base'' s)$ для соответствующих условий.$$

Lean4

/-- **Chevalley's Theorem**: The image of a constructible set under a
morphism of finite presentation into a qcqs scheme is constructible. -/
@[stacks 054J]
theorem isConstructible_image (f : X.Hom Y) [LocallyOfFinitePresentation f] [QuasiCompact f] [CompactSpace Y]
    [QuasiSeparatedSpace Y] {s : Set X} (hs : IsConstructible s) : IsConstructible (f.base '' s) :=
  (f.isLocallyConstructible_image hs.isLocallyConstructible).isConstructible

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