Projective morphisms are proper

The projective bundle P(E) ⟶ X of a quasi-coherent sheaf of finite type is proper (Scheme.Modules.isProper_projectiveBundleπ, as in the proof of [TSPA, Tag 01WC]): over an affine open U with Γ(E, U) finitely generated (such opens cover X, Scheme.Modules.exists_isAffineOpen_finite_sections) it is the projective bundle of the finitely generated module Γ(E, U) over Spec Γ(X, U) ≅ U, which is proper (affineProjectiveBundle.isProper_π), and properness is local on the target. A projective morphism, a closed immersion into such a P(E) followed by P(E) ⟶ X, is therefore proper (AlgebraicGeometry.IsProjective.isProper).

theorem AlgebraicGeometry.Scheme.Modules.isProper_projectiveBundleπ {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] [SheafOfModules.IsFiniteType F] : IsProper F.projectiveBundleπ

The projective bundle of a quasi-coherent sheaf of finite type is proper over the base, as in the proof of [TSPA, Tag 01WC].

@[instance 100]

instance AlgebraicGeometry.IsProjective.isProper {X Y : Scheme} (f : X ⟶ Y) [hf : IsProjective f] : IsProper f

A projective morphism is proper [TSPA, Tag 01WC]: it is a closed immersion into the projective bundle of a quasi-coherent sheaf of finite type followed by the bundle projection, both proper.