The generic point of an irreducible scheme and the specialization order #
The points of a scheme are ordered by specialization: x ≤ y when y generizes x. On an
irreducible scheme the generic point generizes every point, so it is maximal for this order, and
it is the only maximal point: a point with no proper generization is generized by the generic
point and generizes it, hence equals it because the underlying space of a scheme is T₀. Since the
points of coheight zero are the maximal ones, this identifies the points of coheight zero of an
irreducible scheme with its generic point.
Main results #
TauCeti.AlgebraicGeometry.Scheme.isMax_genericPoint: the generic point of an irreducible scheme is maximal for the specialization order;TauCeti.AlgebraicGeometry.Scheme.eq_genericPoint_of_isMax: a point of an irreducible scheme which is maximal for the specialization order is the generic point;TauCeti.AlgebraicGeometry.Scheme.isMax_iff_eq_genericPoint: the maximal points for the specialization order on an irreducible scheme are exactly the generic point.
The generic point of an irreducible scheme is maximal for the specialization order: it generizes every point.
A point of an irreducible scheme which is maximal for the specialization order, that is, a point of coheight zero, is the generic point.
The points of an irreducible scheme which are maximal for the specialization order are exactly the generic point.