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

Proposition 12 (Lecture 8): Projective space is complete. For a graded ring A = ⨁_n 𝒜_n that is of finite type over its degree-zero piece 𝒜 0, the structure morphism Proj 𝒜 → Spec(𝒜 0) is proper. In particular ℙ^n_k → Spec k is proper, so projective space over a field is complete.