Let $X$ be a projective scheme over a field $k$ with $\mathcal{L}$ a very ample line bundle on $X$ (very ample here means relative to the structure morphism $X \to \operatorname{Spec} k$. Where is it located in EGA that the following are equivalent?
- $\mathcal{L}$ is very ample.
- $\bigoplus_{d \geq 0} \Gamma(X,\mathcal{L}^{\otimes d})$ is a finitely generated $k$-algebra, generated in degree $1$.
- The canonical morphism $X \to \operatorname{Proj} \bigoplus_{d \geq 0} \Gamma(X,\mathcal{L}^{\otimes d})$ is an isomorphism.
Presumably this should be a corollary of a more general theorem in EGA, but I can't find this more general theorem.