def Lemma29Completeness.SatisfiesDVRCriterion (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↥X] : Prop

The DVR valuative criterion: every injective map from a DVR to the function field of X extends to a local ring map at some specialization of the generic point (Lemma 29, completeness setting).

theorem Lemma29Completeness.lemma_29_dvr_criterion_iff_complete (X S : AlgebraicGeometry.Scheme) [X.Over S] [IrreducibleSpace ↥X] [AlgebraicGeometry.IsReduced X] : SatisfiesDVRCriterion X ↔ AlgebraicGeometry.IsProper (X ↘ S)

Lemma 29: for an irreducible reduced scheme X over S, the DVR valuative criterion holds iff the structure morphism X ⟶ S is proper (equivalently, X is complete).

theorem Lemma29Completeness.locallyQuasiFinite_of_isIso_fromNormalization {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsDominant f] [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.fromNormalization f)] : AlgebraicGeometry.LocallyQuasiFinite f

Helper for Lemma 29: a proper dominant morphism whose normalization map is an isomorphism is locally quasi-finite.

theorem Lemma29Completeness.lemma_29_birational_complete_normal_isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.IsDominant f] [CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.fromNormalization f)] : CategoryTheory.IsIso f

Lemma 29 (Lec 17): a proper birational morphism to a normal target is an isomorphism.