@[reducible, inline]

abbrev IsVariety (X : Type u) [TopologicalSpace X] : Prop

A variety is a topological space that is Noetherian (every descending chain of closed subsets stabilizes).

class IsCompleteVariety (X : Type u) [TopologicalSpace X] : Prop

A complete variety: a variety $X$ such that the second projection $X \times Y \to Y$ is a closed map for every variety $Y$ (the topological analog of properness).

• isVariety : IsVariety X
• isClosedMap_snd (Y : Type u) [TopologicalSpace Y] [IsVariety Y] : IsClosedMap Prod.snd

theorem IsCompleteVariety_agrees_with_proper {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [IsCompleteVariety ↥X] : AlgebraicGeometry.IsProper f

Compatibility: a complete variety in our topological sense gives a proper morphism to $\mathrm{Spec}(K)$ in the scheme-theoretic sense.

@[instance 100]

instance IsCompleteVariety.toNoetherianSpace {X : Type u} [TopologicalSpace X] [h : IsCompleteVariety X] : TopologicalSpace.NoetherianSpace X

A complete variety is in particular a Noetherian topological space.

instance IsCompleteVariety.of_compactSpace {X : Type u} [TopologicalSpace X] [CompactSpace X] [TopologicalSpace.NoetherianSpace X] : IsCompleteVariety X

Any compact Noetherian space is a complete variety, since the projection $X \times Y \to Y$ from a compact space is automatically closed.

theorem IsCompleteVariety.lemma_16_12 {X : Type u} [TopologicalSpace X] [hX : IsCompleteVariety X] {Y : Type u} [TopologicalSpace Y] [IsVariety Y] {φ : X → Y} (hφ : Continuous φ) (hgraph : IsClosed {p : X × Y | p.2 = φ p.1}) : IsClosedMap φ ∧ IsCompleteVariety ↑(Set.range φ)

(Lemma 16.12) If $X$ is a complete variety and $\varphi : X \to Y$ is a continuous map with closed graph, then $\varphi$ is a closed map and its image is a complete variety.

theorem IsCompleteVariety.isCompleteVariety_of_isClosed {X : Type u} [TopologicalSpace X] [hX : IsCompleteVariety X] {V : Set X} (hV : IsClosed V) : IsCompleteVariety ↑V

A closed subset of a complete variety is itself a complete variety.

theorem complete_affine_variety_subsingleton {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsProper f] : Subsingleton ↥X

A complete affine integral variety over a field $K$ is a single point: if $X$ is affine, integral, and $X \to \mathrm{Spec}(K)$ is proper, then $X$ is a subsingleton.