felixwellen
commented
7 months ago Another approach would be to find an (external) counterexample, which would be a non-trivial map $\mathbb A^1\to B\widetilde{\mathbb A^\times}$. We could start by looking at base rings with non-trivial picard group, construct a non-trivial line bundle on $\mathbb A^1$ from that and see if it is still non-trivial if we formally étale replace the lines.
Formulated more in line with the A1-homotopy draft: Is $B\widetilde{\mathbb A^\times}$ an $\mathbb A^1$-local type? Using reasoning from 2.2 in the A1-homotopy draft, it is enough to show that $H^1(\mathbb A^1,\widetilde{\mathbb A^\times})=0$.