Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image

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

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

Defined in

Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.LocallyOfFinitePresentationAlgebraicGeometry.QuasiCompact