The projective bundle of a quasi-coherent sheaf, and projective morphisms

For a quasi-coherent sheaf of modules F on a scheme X (Mathlib's X.Modules with SheafOfModules.IsQuasicoherent), the projective bundle P(F) = Proj_X (Sym F) [TSPA, Tag 01OB] is F.projectiveBundle, with structure morphism F.projectiveBundleπ : P(F) ⟶ X. It is glued by the relative gluing lemma [TSPA, Tag 01LH] from the projective bundles P(Γ(F, U)) = Proj (Sym_{Γ(X, U)} Γ(F, U)) of the modules of sections over the affine opens U of X (projectiveBundleFunctor F, projectiveBundleNatTrans F), whose naturality squares are pullbacks by quasi-coherence (projectiveBundleNatTrans_equifibered), as the blow-up is glued from the affine blow-ups.

A morphism f : X ⟶ Y is projective (AlgebraicGeometry.IsProjective) [TSPA, Tag 01W8] when X is isomorphic over Y to a closed subscheme of the projective bundle P(E) of a quasi-coherent 𝒪_Y-module E of finite type: f is a closed immersion X ⟶ P(E) followed by P(E) ⟶ Y.

noncomputable def AlgebraicGeometry.projectiveBundleGluingData {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : Scheme.Cover.RelativeGluingData X.directedAffineCover

The relative gluing datum of the projective bundles over the directed affine cover [TSPA, Tag 01LH].

Equations

• AlgebraicGeometry.projectiveBundleGluingData F = { functor := AlgebraicGeometry.projectiveBundleFunctor F, natTrans := AlgebraicGeometry.projectiveBundleNatTrans F, equifibered := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.projectiveBundle {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : Scheme

The projective bundle P(F) = Proj_X (Sym F) of a quasi-coherent sheaf of modules F [TSPA, Tag 01OB]: glued from the projective bundles Proj (Sym_{Γ(X, U)} Γ(F, U)) of the modules of sections over the affine opens U of X.

Equations

• F.projectiveBundle = (AlgebraicGeometry.projectiveBundleGluingData F).glued

noncomputable def AlgebraicGeometry.Scheme.Modules.projectiveBundleπ {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : F.projectiveBundle ⟶ X

The structure morphism P(F) ⟶ X of the projective bundle.

Equations

• F.projectiveBundleπ = (AlgebraicGeometry.projectiveBundleGluingData F).toBase

class AlgebraicGeometry.IsProjective {X Y : Scheme} (f : X ⟶ Y) : Prop

A projective morphism [TSPA, Tag 01W8]: f : X ⟶ Y is projective when X is isomorphic over Y to a closed subscheme of the projective bundle P(E) of a quasi-coherent 𝒪_Y-module E of finite type, that is, when f factors as a closed immersion X ⟶ P(E) followed by the structure morphism P(E) ⟶ Y. A projective morphism is proper (AlgebraicGeometry.IsProjective.isProper).

Relation to the source.

• Translation. Kollár's "projective morphism" [Kol07, (2) and (3); Theorem 27] is IsProjective, Grothendieck's definition as in [TSPA, Tag 01W8]: E ranges over the quasi-coherent 𝒪_Y-modules of finite type (Mathlib's SheafOfModules.IsQuasicoherent and SheafOfModules.IsFiniteType). Kollár's varieties are quasi-projective, and over a base with an ample invertible sheaf this is equivalent to being a closed subscheme of some ℙⁿ_Y [TSPA, Tag 087S]; for a general base the condition with ℙⁿ_Y is stronger, and the condition on an open cover of Y only ("locally projective") is weaker [TSPA, Tag 01W8], a distinction Kollár draws in [Kol07, Example 28.1].

• exists_isClosedImmersion : ∃ (E : Y.Modules) (x : SheafOfModules.IsQuasicoherent E) (_ : SheafOfModules.IsFiniteType E) (i : X ⟶ E.projectiveBundle), IsClosedImmersion i ∧ CategoryTheory.CategoryStruct.comp i E.projectiveBundleπ = f