@[reducible, inline]

noncomputable abbrev SeparatednessDefinition.SpecK (k : Type u) [Field k] : AlgebraicGeometry.Scheme

The base scheme Spec k for varieties over a field k.

@[reducible, inline]

abbrev SeparatednessDefinition.IsSeparatedVariety (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ SpecK k) : Prop

A k-variety X (with structure morphism f : X → Spec k) is separated when f is a separated morphism.

noncomputable def SeparatednessDefinition.diagonalMorphism (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ SpecK k) : X ⟶ CategoryTheory.Limits.pullback f f

The diagonal morphism Δ : X → X ×_{Spec k} X of a k-variety.

theorem SeparatednessDefinition.isSeparatedVariety_iff_diagonal_isClosedImmersion (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ SpecK k) : IsSeparatedVariety k f ↔ AlgebraicGeometry.IsClosedImmersion (diagonalMorphism k f)

Separatedness criterion: a k-variety is separated iff its diagonal morphism Δ : X → X × X is a closed immersion.

theorem SeparatednessDefinition.affine_isSeparated (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : X ⟶ SpecK k) : IsSeparatedVariety k f

Any affine k-variety is separated.

theorem SeparatednessDefinition.affine_diagonal_isClosedImmersion (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : X ⟶ SpecK k) : AlgebraicGeometry.IsClosedImmersion (diagonalMorphism k f)

For an affine k-variety, the diagonal is automatically a closed immersion.