Large ample twists of a line bundle are very ample

Given: a field $k$, an integral smooth projective surface $X$ over $k$, an ample invertible sheaf $L$ and an invertible sheaf $M$ on $X$.

Serre's global-generation criterion: on the Noetherian scheme $X$ the invertible sheaf $L$ is ample if and only if for every coherent ${\mathcal{O}}_X$-module $F$ the twist $F\otimes L^{\otimes n}$ is globally generated for all sufficiently large $n$ (Serre global-generation criterion for ampleness, Locally Noetherian and Noetherian schemes). The invertible sheaf $M$ is coherent on the locally Noetherian scheme $X$, and $X$ is quasi-compact, so global generation of an invertible sheaf is witnessed by finitely many global sections (Global generation by the evaluation map, Invertible sheaves).

Ample powers embed: $\mathrm{Spec}k$ is Noetherian, $X\to \mathrm{Spec}k$ is proper of finite type, and $L$ is ample, so there is an integer $d_0\ge 1$ such that $L^{\otimes d}$ is closed H-very ample relative to $\mathrm{Spec}k$ for every $d\ge d_0$ (High powers of an ample line bundle embed a proper scheme, Projective morphisms before Proj). Concretely this means that for each such $d$ there is a closed immersion $i_d:X\hookrightarrow {\mathbb{P}}_k^{N_d}$ with $i_d^{\ast }\mathcal{O}(1)\cong L^{\otimes d}$ (Relative very ampleness in the finite projective-space convention).

Generating sections define a morphism: if $s_0,\dots ,s_p$ are global sections generating an invertible sheaf $G$, there is a unique $k$-morphism $\phi :X\to {\mathbb{P}}_k^p$ with ${\phi }^{\ast }\mathcal{O}(1)\cong G$ and ${\phi }^{\ast }(x_i)=s_i$ (Generating line-bundle sections define a morphism to projective space).

Graphs and immersions: for a $k$-morphism $u:X\to Y$ with $Y$ separated over $k$ the graph ${\mathrm{\Gamma }}_u:X\to X{\times }_{k}Y$ is a closed immersion, because the defining square is a base change of the diagonal ${\mathrm{\Delta }}_{Y\mathrm{/}k}$ (The graph is a pullback of the diagonal, Separated morphism of schemes) and base changes of closed immersions are closed immersions (Closed immersions are affine quotients and survive base change); the projective space ${\mathbb{P}}_k^p$ is proper over $k$, hence separated (Finite-dimensional projective space is proper over every base, Separated morphism of schemes), and a composite of closed immersions is a closed immersion, since the composite of homeomorphisms onto closed subsets is again one and a composite of surjective sheaf maps is surjective (Closed immersions of schemes). The canonical swap $X{\times }_k{\mathbb{P}}_k^p\to {\mathbb{P}}_k^p{\times }_{k}X$ is an isomorphism, so it preserves closed immersions.

The Segre embedding: with $p,q\ge 0$ and $P={\mathbb{P}}_k^p{\times }_k{\mathbb{P}}_k^q$ with projections ${\mathrm{p}\mathrm{r}}_1,{\mathrm{p}\mathrm{r}}_2$, there is a closed immersion $\sigma :P\hookrightarrow {\mathbb{P}}_k^{(p+1)(q+1)-1}$ with ${\sigma }^{\ast }\mathcal{O}(1)\cong {\mathrm{p}\mathrm{r}}_1^{\ast }\mathcal{O}(1)\otimes {\mathrm{p}\mathrm{r}}_2^{\ast }\mathcal{O}(1)$ (Segre embedding and its line bundle).

The Axiom of Choice is inherited from the Proj, ample-embedding and Segre suppliers of [F2], [F4] and [F5]; the finitely many generating sections chosen in step 3.1 are a finite family, and no infinite selection occurs.