Mathlib's SymmetricAlgebra R M is the free commutative R-algebra on an R-module M; the library grades it. The n-th piece SymmetricAlgebra.grading R M n is \operatorname{Sym}^n M = \iota(M)^n, the n-th power of the submodule spanned by the image of M; the lift of the inclusion of M in degree one into the direct sum of the pieces (SymmetricAlgebra.gradedι) splits the inclusion of the direct sum, which makes it a graded algebra (SymmetricAlgebra.gradedAlgebra). The degree-zero piece is R (SymmetricAlgebra.gradingZeroEquiv).

A ring map \varphi \colon R \to S and a \varphi-semilinear map f \colon M \to N induce the graded ring map \operatorname{Sym}_R M \to \operatorname{Sym}_S N, \iota m \mapsto \iota f(m) (SymmetricAlgebra.gradedMap), the lift of m \mapsto \iota f(m) for the R-algebra structure of \operatorname{Sym}_S N along \varphi (SymmetricAlgebra.algebraOfRingHom, SymmetricAlgebra.ιₛₗ).

The projective bundle of an R-module M is \mathbf{P}(M) = \operatorname{Proj}(\operatorname{Sym}_R M) (affineProjectiveBundle R M), with the structure morphism to \operatorname{Spec} R induced by R \cong \operatorname{Sym}^0 M (affineProjectiveBundle.π). For M = R^n it is projective space \mathbb{P}^{n-1}_R. A ring map \varphi \colon R \to S and a \varphi-semilinear map f \colon M \to N whose image spans N induce \mathbf{P}(N) \to \mathbf{P}(M) over \operatorname{Spec} \varphi (affineProjectiveBundle.map, and affineProjectiveBundle.mapHom for a morphism of CommRingCat): Mathlib's Proj.map of the graded map, whose hypothesis — the irrelevant ideal of \operatorname{Sym}_S N, generated by \iota(N), lies in the ideal generated by the image of that of \operatorname{Sym}_R M — is the spanning.

When f exhibits N as S \otimes_R M, the square of \mathbf{P}(N) \to \mathbf{P}(M) over \operatorname{Spec} S \to \operatorname{Spec} R is cartesian [TSPA, Tag 01N2] (affineProjectiveBundle.isPullback_map). On the chart D_+(\iota x) of \mathbf{P}(M) this is a pushout of rings: the degree-zero part (\operatorname{Sym} M)_{(\iota x)} of the localization at \iota x is the free commutative R-algebra on M with x = 1, its elements being the fractions a / (\iota x)^n, a \in \operatorname{Sym}^n M (SymmetricAlgebra.awayLift, SymmetricAlgebra.isPushout_away).

The projective bundle of a quasi-coherent sheaf of modules \mathcal{E} on X is \mathbf{P}(\mathcal{E}) = \operatorname{Proj}_X (\operatorname{Sym} \mathcal{E}) (E.projectiveBundle), with projection E.projectiveBundleπ to X [TSPA, Tag 01OB]. It is glued by the relative gluing lemma [TSPA, Tag 01LH] from the functor projectiveBundleFunctor on the affine opens of X, U \mapsto \mathbf{P}(\Gamma(\mathcal{E}, U)), whose transition maps are induced by the restrictions \Gamma(\mathcal{E}, V) \to \Gamma(\mathcal{E}, U), semilinear along \Gamma(X, V) \to \Gamma(X, U) (Scheme.Modules.restrictionMap), and from the structure morphisms \mathbf{P}(\Gamma(\mathcal{E}, U)) \to \operatorname{Spec} \Gamma(X, U) \cong U (projectiveBundleNatTrans), whose naturality squares are pullbacks by quasi-coherence (projectiveBundleNatTrans_equifibered; projectiveBundleGluingData).

A morphism f \colon X \to Y is projective (IsProjective f) if X is isomorphic over Y to a closed subscheme of the projective bundle \mathbf{P}(\mathcal{E}) of a quasi-coherent \mathcal{O}_Y-module \mathcal{E} of finite type: f is a closed immersion X \to \mathbf{P}(\mathcal{E}) followed by the projection [TSPA, Tag 01W8]. This is Grothendieck's definition, and the reading of Kollár's "projective morphism". Over a base with an ample invertible sheaf, a quasi-projective variety over a field for instance, it agrees with being a closed subscheme of some \mathbb{P}^n_Y [TSPA, Tag 087S]; in general that condition is stronger, while asking the condition only over the members of an open cover of Y, locally projective, is weaker, and Kollár's Example 28.1 is a proper, locally projective morphism that is not projective [Kol07, Example 28.1].

A projective morphism is proper (IsProjective.isProper): \mathbf{P}(\mathcal{E}) \to Y is proper for \mathcal{E} of finite type (as in the proof of [TSPA, Tag 01WC]), being, over an affine open with finitely generated sections, \operatorname{Proj} of a graded algebra generated by finitely many elements of degree one. A blow-up of a locally Noetherian scheme along an ideal sheaf \mathcal{I} is projective (Scheme.IdealSheafData.isProjective_blowUpπ, [TSPA, Tag 02NS]): the surjection \operatorname{Sym} \mathcal{I} \to \bigoplus_n \mathcal{I}^n, the identity of \mathcal{I} in degree one, makes it a closed subscheme of \mathbf{P}(\mathcal{I}), the ideal sheaf being a quasi-coherent sheaf of modules of finite type. As a finite succession of blow-ups of a Noetherian scheme is one blow-up [TSPA, Tag 080B], its composite is projective (Scheme.BlowUpSequence.isProjective_composite).