Fundamental group of a product in characteristic 0

It is proven in SGA1 that if $$k$$ is an algebraically closed field, if $$X$$ is a proper $$k$$-scheme and if $$Y$$ is a locally noetherian $$k$$-scheme (say, $$X$$ and $$Y$$ are non-empty and connected) then $$\pi_1(X\times_k Y)=\pi_1(X)\times \pi_1(Y)$$. This implies that if $$L$$ is any algebraically closed extension of $$k$$ then $$\pi_1(X\times_k L)=\pi_1(X)$$. All of these results are known to fail without the properness assumption, but all counter-examples are in positive characteristic, and I am almost sure that this assumption can be removed in char. $$0$$.

Question: is it written somewhere? I did not find any proof of it in SGA, nor in Stacks Project.

For the commutation with the product over $$\mathbb C$$ one can use the corresponding result in topology and the comparison theorem between étale and topological fundamental groups, but reducing the case of an arbitrary algebraically closed field of char. 0 to that of $$\mathbb C$$ would first require a proof of the invariance of the $$\pi_1$$ under algebraically closed extension.

• The invariance of fundamental groups under extensions of alg. closed fields in char. 0 is discussed here. Since then Aaron Landesman has also written up a proof of the invariance here: arxiv.org/pdf/2005.09690.pdf – Will Chen Dec 16 '20 at 23:36
• Thank you very much! The quasi-projectivity assumption in the ArXiv paper you refer to looks strange. I think it is probably not necessary? – Antoine Ducros Dec 18 '20 at 10:04
• @AntoineDucros it seems that by van Kampen it suffices to treat the affine case? – Piotr Achinger Dec 18 '20 at 19:58