isConstructible_range_comap — Mathlib

English

For a finite presentation morphism f : R →+* S, the range of the contraction comap f is a constructible subset of Spec(R).

Русский

Для морфинфизма f: R →+* S конечной презентации множество образов через comap f является конструктивным подмножеством Spec(R).

LaTeX

$$$f.FinitePresentation \\Rightarrow \\operatorname{IsConstructible}(\\operatorname{range}(\\operatorname{comap} f))$$

Lean4

theorem isConstructible_range_comap {f : R →+* S} (hf : f.FinitePresentation) :
    IsConstructible (Set.range <| comap f) :=
  Set.image_univ ▸ isConstructible_comap_image hf .univ

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