Finite translate completion and uniqueness

Successively glue translates $X^{(i+1)}=X^{(i)}\cup X^{(i)}(a_{i+1})$ whenever a section translation of the original $X$ is not defined everywhere as a map $X⇢X^{(i)}$. Let $Q_i\subseteq X\times X$ be the domain of its original multiplication with values in $X^{(i)}$. By the graph open-immersion property [F1] these are increasing opens of the fixed Noetherian scheme $X\times X$. If the next translation is undefined at $b$, its newly glued translate defines it there; graph calculus then puts $(a_{i+1},b)$ in $Q_{i+1}\setminus Q_i$. Such strict increases cannot continue indefinitely in a Noetherian space. Thus for a finite enlargement $Y$, every original section translation $t_a:X\to Y$ is everywhere defined.

Fix a geometric pair $(x,y)$ in $X\times X$. Strict graph calculus [F1] makes the auxiliary locus of $w$ where $w^{-1}x\in X$ and $(w^{-1}x,y)$ is in the original law domain open and fibre-dense in $X$. By [F2] some section $a$ meets this locus: on the special fibre use smooth section lifting, and on the generic fibre use the generic-open assertion on a component with nonempty special fibre. Then the map $(x,y)\mapsto a((a^{-1}x)y)$ is defined near the pair, since its inner product lies in the original $X$ and $t_a:X\to Y$ is everywhere defined by step 1.1. Associativity identifies this map with the original rational multiplication. It follows that the extended strict law on $Y$ is a morphism on the entire original $X\times X$.

To extend the law to all of $Y\times Y$, choose an auxiliary $a\in X$ at a generic point of the fibre over a given pair $(b,c)\in Y\times Y$. The strict graph projections [F1] put $ba\in X$ and $a^{-1}c\in X$ on a fibre-dense open auxiliary locus. Their product is defined by step 2.1, and associativity gives $bc=(ba)(a^{-1}c)$. This gives the rational law a regular representative on a smooth faithfully flat auxiliary cover, so domain descent [F2] makes it regular at $(b,c)$. The same argument makes the division map $(b,c)\mapsto b^{-1}c$ regular everywhere. The strict translation monomorphism into the relative birational-map group, supplied by [F1], now identifies $Y(T)$ with a subset closed under multiplication and division for every test $T$. It is nonempty since faithful flatness and smoothness over the strictly henselian DVR give an $R^{\mathrm{s}\mathrm{h}}$-section. Hence it is a subgroup: division gives the unit and inverses, and associativity holds by the strict law and schematic density. These natural operations are scheme morphisms by their construction, so $Y$ is the claimed smooth separated finite-type group completion.

For uniqueness over a base $S$, let $Y_1,Y_2$ be smooth separated finitely presented group completions containing the same smooth faithfully flat finitely presented fibre-dense $X$. Each $Y_i$ acts faithfully by birational translations on $X_T$ for every test $T$: the domain $X_T\cap y^{-1}{X}_T$ is fibre-dense, and equality of translations implies equality of the translating sections after the faithfully flat dense domain cover of $T$. The multiplication map $q_i:X{\times }_{S}X\to Y_i$ is smooth, since it is a restriction of group multiplication, and surjective: in each geometric fibre, for a prescribed $y$, the dense opens $X$ and $y{X}^{-1}$ intersect. It is quasi-compact and locally finitely presented. On the kernel pair of $q_1$, two pairs from $X^2$ have the same product in $Y_1$, hence the same product of birational translations of $X$ by [F1]; faithfulness for $Y_2$ makes their $q_2$-images equal. Fppf morphism descent [F2] gives $Y_1\to Y_2$ with composite $q_1$ equal to $q_2$. Reversing the roles gives an inverse, by surjectivity of the covers. The isomorphism fixes $X$ (compare translations, using their faithful action) and preserves group multiplication by the same comparison. Faithfulness also proves uniqueness. This proof applies to arbitrary pullback bases, including the tensor-product bases used for descent.