theorem lemma_16_32 {F : Type u_1} [Field F] (R : ValuationSubring F) (n : ℕ) (x : Fin (n + 1) → F) (hx : ∀ (i : Fin (n + 1)), x i ≠ 0) : ∃ (l : F), l ≠ 0 ∧ (∀ (i : Fin (n + 1)), l * x i ∈ ↑R) ∧ ∃ (i : Fin (n + 1)), (l * x i)⁻¹ ∈ ↑R

(Lemma 16.32) Given a valuation subring $R \subseteq F$ and finitely many nonzero $x_0, \dots, x_n \in F$, there exists $\lambda \in F^\times$ such that $\lambda x_i \in R$ for all $i$ and some $\lambda x_i$ is a unit in $R$ (this normalises projective coordinates with respect to a valuation).

structure AlgebraicGeometry.CompletenessValuationCriterion.IsProjectiveVariety {k : Type u} [Field k] (V : AlgVariety k) : Type (u + 1)

A projective variety structure on $V$: a choice of dimension $n$ and homogeneous coordinates $X_0, \dots, X_n \in K(Z)^\times$ (none vanishing) on every subvariety $Z$ of $V$.

• n : ℕ
• homogCoords (Z : SubvarietyOf V) : Fin (self.n + 1) → Z.toVariety.functionField
• homogCoords_ne_zero (Z : SubvarietyOf V) (i : Fin (self.n + 1)) : self.homogCoords Z i ≠ 0

theorem AlgebraicGeometry.CompletenessValuationCriterion.affineChartLocalRing {k : Type u} [Field k] {V : AlgVariety k} (hproj : IsProjectiveVariety V) (Z : SubvarietyOf V) (j : Fin (hproj.n + 1)) (R : ValRingOver Z.toVariety) (hcoords : ∀ (i : Fin (hproj.n + 1)), hproj.homogCoords Z i * (hproj.homogCoords Z j)⁻¹ ∈ R.valSub) : ∃ (P : Z.toVariety.carrier), localRing_le P R

If all ratios $X_i / X_j$ lie in the valuation ring, then the valuation is dominated by the local ring of some point of the affine chart $\{X_j \neq 0\}$.

theorem AlgebraicGeometry.CompletenessValuationCriterion.pointFromScaledCoords_lemma {k : Type u} [Field k] {V : AlgVariety k} (hproj : IsProjectiveVariety V) (Z : SubvarietyOf V) (R : ValRingOver Z.toVariety) (l : Z.toVariety.functionField) (hl_ne : l ≠ 0) (hl_mem : ∀ (i : Fin (hproj.n + 1)), l * hproj.homogCoords Z i ∈ R.valSub) (hl_unit : ∃ (i : Fin (hproj.n + 1)), (l * hproj.homogCoords Z i)⁻¹ ∈ R.valSub) : ∃ (P : Z.toVariety.carrier), localRing_le P R

If some scaling $\lambda X_i$ of the homogeneous coordinates lies in $R$ with some $\lambda X_j$ a unit, then $R$ is dominated by a point of $Z$.

theorem AlgebraicGeometry.CompletenessValuationCriterion.projective_variety_satisfies_valuation_criterion {k : Type u} [Field k] (V : AlgVariety k) (hproj : IsProjectiveVariety V) : SatisfiesValuationCriterion V

A projective variety satisfies the valuation criterion of properness.

theorem AlgebraicGeometry.CompletenessValuationCriterion.projective_variety_isComplete {k : Type u} [Field k] [IsAlgClosed k] (V : AlgVariety k) (hproj : IsProjectiveVariety V) : IsCompleteVariety V.carrier

Projective varieties are complete: over an algebraically closed field, every projective variety satisfies the topological completeness condition.

theorem theorem_16_33 {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : AlgebraicGeometry.IsProper (AlgebraicGeometry.Proj.toSpecZero 𝒜)

(Theorem 16.33) The structure morphism $\mathrm{Proj}\,\mathcal{A} \to \mathrm{Spec}\,\mathcal{A}_0$ from a finitely generated $\mathbb{N}$-graded ring is proper.