def SeparatedHausdorff.complexPoints (X : AlgebraicGeometry.Scheme) : Type

Complex points of a scheme X: morphisms Spec ℂ → X.

noncomputable def SeparatedHausdorff.classicalTopology (X : AlgebraicGeometry.Scheme) (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : TopologicalSpace (complexPoints X)

Classical (analytic) topology on the complex points of a reduced, locally-finite-type ℂ-scheme.

theorem SeparatedHausdorff.separated_imp_diagonal_closed {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : X.IsSeparated → IsClosed (Set.diagonal (complexPoints X))

Forward direction of the separated-iff-Hausdorff equivalence: if X is separated, then the diagonal in X(ℂ) × X(ℂ) is closed for the classical topology.

theorem SeparatedHausdorff.diagonal_closed_imp_separated {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : IsClosed (Set.diagonal (complexPoints X)) → X.IsSeparated

Reverse direction: closedness of the diagonal in the classical topology implies X is separated as a scheme.

theorem SeparatedHausdorff.separated_iff_hausdorff_classical {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : X.IsSeparated ↔ T2Space (complexPoints X)

X is separated as a ℂ-scheme iff X(ℂ) is Hausdorff for the classical topology.

theorem SeparatedHausdorff.goal71_separated_iff_hausdorff {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of ℂ)) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.IsReduced X] : X.IsSeparated ↔ T2Space (complexPoints X)

Goal 7.1: equivalence between scheme-theoretic separatedness and the Hausdorff property of complex points (restated under the goal name).