def AlgebraicGeometry.CompletenessValuationCriterion.pointAlgVariety (k : Type u) [Field k] : AlgVariety k

The one-point algebraic variety: $\mathrm{Spec}(k)$ as an AlgVariety, with function field $k$ and the trivial topology.

def AlgebraicGeometry.CompletenessValuationCriterion.pointIsProjectiveVariety (k : Type u) [Field k] : IsProjectiveVariety (pointAlgVariety k)

The point is a projective variety: $\mathrm{Spec}(k) = \mathbb{P}^0$, with the unique homogeneous coordinate $1 \neq 0$.

def IsProjectiveVariety.punit (k : Type u) [Field k] [IsAlgClosed k] : IsProjectiveVariety k PUnit.{u + 1}

$\mathrm{PUnit}$ (the one-point space) is a projective variety over any algebraically closed field $k$.