$\mathbb{A}^1$-invariance of categories of Finite Etale Covers

Question

Let $k$ be algebraically closed with characteristic $0$. For a scheme $X$, let $FEt(X)$ be the category of finite etale covers of $X$. What can be said about $FEt(X \times \mathbb{A}^1)$ and the functor $- \times_k \mathbb{A}^1: FEt(X) \rightarrow FEt(X \times \mathbb{A}^1)$?

It seems to me that the functor induced by pullback along the zero section $0: X \rightarrow X \times_k \mathbb{A}^1$, $FEt(X \times \mathbb{A}^1) \rightarrow FEt(X)$ witnesses a fully faithful embedding since the composite of this with the one above is the identity, but that's about all I can observe immediately.

So is the functor an equivalence/final/cofinal?

At least, the etale fundamental group is $\mathbb{A}^1$-invariant for suitably nice $X$ (the etale fundamental group preserves products for suitably nice $X$ and the etale fundamental group of $\mathbb{A}^1$ is zero) and so is the etale homotopy type after appropriate completion. Can one perhaps lift this to some equivalence between etale covers?

Answer 1

I'm a bit surprised that this was never answered - if I'd known I'd posted something more helpful than a snippy question. Yes, $FEt(X) \to FEt(X \times \mathbb A^1)$ is an equivalence of categories in characteristic zero. This assertion is in fact equivalent to $\pi_1^{et}(X) \to \pi_1^{et}(X \times \mathbb A^1)$ being an isomorphism, a fact you seem comfortable with. An isomorphism between the respective fundamental groups necessarily induces an equivalence between the categories of finite continuous $\pi_1$-sets, which in turn are canonically equivalent to the categories of finite étale covers once we've fixed a base point. In positive characteristic you'd have to consider instead the tame fundamental group.