Smooth proper specialization of the étale fundamental group

Apply [F1] to reduce to a smooth proper trait family $X\mathrm{/}R$ with algebraically closed residue field and geometric generic fibre $X_{\bar{K}}$. Choose the basepoint identifications in that reduction. The cover equivalence $\mathrm{FEt}(X)\simeq \mathrm{FEt}(X_k)$ of [F2] defines the specialization map by first pulling an extended special cover back to the geometric generic fibre; on fundamental groups this is the indicated generic-to-special direction. The connectedness assertion of [F2] proves surjectivity. If the two original points coincide, [F1] identifies it with a path isomorphism, already satisfying every conclusion.

Let $G$ be a finite group whose order is prime to $p=\mathrm{char}k>0$, or any finite group if $\mathrm{char}k=0$. A continuous homomorphism from ${\pi }_1(X_{\bar{K}})$ to $G$ is represented by a finite étale $G$-torsor via [F2]. It descends to $X_L$ for a finite separable extension $L\mathrm{/}K$: the finitely many presentations, gluing maps, group-action maps and torsor identities on a finite affine cover and its intersections involve only finitely many coefficients. A finite purely inseparable part can be discarded by unique étale lifting along radicial field extensions, which is part of [F1]'s geometric-field invariance. Replace $R$ by its complete DVR normalization $R^{\mathrm{\prime }}$ in $L$, and normalize $X_{R^{\mathrm{\prime }}}$ in the generic torsor algebra. By [F4] that normalization is finite and normal. The total space $X_{R^{\mathrm{\prime }}}$ is regular, by the smooth-over-regular-base argument in [F2]'s proper-cover proof. The cover is already étale over the generic fibre; its only possible codimension-one ramification is vertical.

Apply [F3] to a further finite trait extension $R^{\mathrm{\prime }\mathrm{\prime }}\mathrm{/}{R}^{\mathrm{\prime }}$ to kill that vertical tame ramification. Normalize again, using [F4]. The result is finite normal and étale at every codimension-one point: the horizontal ones lie over the generic fibre, and the vertical ones are unramified by [F3] and hence étale over their DVR bases. Purity in [F4] makes the whole cover finite étale over $X_{R^{\mathrm{\prime }\mathrm{\prime }}}$. Its $G$-action extends uniquely by normalization, and the torsor identity extends because both sides are finite étale covers and their morphism is an isomorphism on the dense generic fibre. By [F2], restriction to the closed fibre is an equivalence for both $X_R$ and $X_{R^{\mathrm{\prime }\mathrm{\prime }}}$; their common closed fibre is $X_k$. Hence this $G$-torsor is the pullback of one on $X_R$ determined by that closed torsor, and its geometric generic fibre is the original torsor. Thus every such homomorphism to $G$ factors through specialization (with the stated basepoint-path conventions).

In characteristic zero, step 3.1 applies to every finite quotient of the profinite generic fundamental group. Its kernel under specialization lies in the intersection of the kernels of all finite quotient maps, which is trivial for a profinite group by [F2]. Together with surjectivity this proves the full isomorphism. In characteristic $p>0$, the same argument applies exactly to all finite quotients of order prime to $p$. Factorization in step 3.1 and surjectivity in step 1.1 identify the finite continuous prime-to-$p$ quotient systems of the generic and special groups, including their transition maps. Their inverse limits are therefore canonically isomorphic as profinite groups. Transporting this back through [F1] proves the complete original statement. The AC use is precisely [F5].