The projective bundles over the affine opens

For a quasi-coherent sheaf of modules F on a scheme X, the projective bundle P(F) = Proj_X (Sym F) [TSPA, Tag 01OB] is glued 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, as the blow-up is glued from the affine blow-ups:

• AlgebraicGeometry.projectiveBundleFunctor F : U ↦ affineProjectiveBundle Γ(X, U) Γ(F, U), with transition map for U ≤ V the morphism P(Γ(F, U)) ⟶ P(Γ(F, V)) induced by the restriction Γ(F, V) → Γ(F, U) (Scheme.Modules.restrictionMap), semilinear along Γ(X, V) → Γ(X, U); its image spans Γ(F, U) by quasi-coherence (Scheme.Modules.span_range_restrictionMap_eq_top), the hypothesis of Proj.map;
• AlgebraicGeometry.projectiveBundleNatTrans F: the structure morphisms P(Γ(F, U)) ⟶ Spec Γ(X, U) ≅ U, natural in U, to the diagram of the directed cover of X by its affine opens.

noncomputable def AlgebraicGeometry.projectiveBundleFunctor {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : CategoryTheory.Functor (↑X.affineOpens) Scheme

The functor of projective bundles on the affine opens of X, U ↦ P(Γ(F, U)) = Proj (Sym_{Γ(X, U)} Γ(F, U)), with transition map for U ≤ V the morphism induced by the restriction Γ(F, V) → Γ(F, U) [TSPA, Tags 01OB and 01LH].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.projectiveBundleNatTrans {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : projectiveBundleFunctor F ⟶ Scheme.Cover.functorOfLocallyDirected X.directedAffineCover

The structure morphisms P(Γ(F, U)) ⟶ Spec Γ(X, U) ≅ U, as a natural transformation to the directed affine cover's diagram [TSPA, Tag 01LH].

Equations

• One or more equations did not get rendered due to their size.