The projective bundles over the affine opens glue

For a quasi-coherent sheaf F and affine opens U ≤ V of X, the square

P(Γ(F, U)) ⟶ U
     |         |
P(Γ(F, V)) ⟶ V

is cartesian (AlgebraicGeometry.projectiveBundleNatTrans_equifibered), the hypothesis of the relative gluing lemma [TSPA, Tag 01LH]: Γ(F, U) is the base change Γ(X, U) ⊗_{Γ(X, V)} Γ(F, V) (Scheme.Modules.isBaseChange_resₗ), so the projective bundles commute with the base change Spec Γ(X, U) ⟶ Spec Γ(X, V) (affineProjectiveBundle.isPullback_mapHom), and that square is pasted with the square of isomorphisms Spec Γ(X, U) ≅ U, Spec Γ(X, V) ≅ V over U ⊆ V.

theorem AlgebraicGeometry.projectiveBundleNatTrans_equifibered {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] : CategoryTheory.NatTrans.Equifibered (projectiveBundleNatTrans F)

The projective bundles over the affine opens glue: every naturality square of projectiveBundleNatTrans F is a pullback [TSPA, Tags 01MX and 01LH].