Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.isConstructible_image

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f]
  [AlgebraicGeometry.QuasiCompact f] [CompactSpace ↥Y] [QuasiSeparatedSpace ↥Y] {s : Set ↥X},
  Topology.IsConstructible s → Topology.IsConstructible (⇑f '' s)

Chevalley's Theorem: The image of a constructible set under a morphism of finite presentation into a qcqs scheme is constructible.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Cited by

0 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.LocallyOfFinitePresentationAlgebraicGeometry.QuasiCompactCompactSpaceQuasiSeparatedSpace