@Zhen Lin,

not sure what you are trying me to do. But you can hit the edit button and do it yourself!

]]>@David,

I am still lacking a good feeling for how to think of $p$-adic stuff in the grand scheme of things.

Also the real numbers have been formalized in HoTT, in

- Univalent Foundations Project, chapter 11 of
*Homotopy Type Theory – Univalent Foundations of Mathematics*

Does considering these two formalizations carry any message beyond that it can be done? Is one somehow “more fundamental” or “more natural” from the perspective of HoTT?

Does anyone have an idea?

]]>It is quite misleading to talk about étale cohomology with coefficients in $\mathbb{F}_p$, $\mathbb{Z}_p$, and $\mathbb{Q}_p$ all in the same breath, when each one is constructed in a different way!

]]>I wonder if the Coq-formulation of the p-adics here is going to be important. They say they’re looking to move towards p-adic symplectic geometry.

]]>added a few more lines as such:

Specifically, let $A$ be either of

the p-adic integers $\mathbb{Z}_p$ for some prime $p \geq 2$;

the p-adic numbers $\mathbb{A}_{p}$

(but *not* for instance the integers themselves).

Then for $X$ a variety over the complex numbers and $X(\mathbb{C})$ its topological space of complex point there is an isomorphism

$H^\bullet(X_{et}, A) \simeq H^\bullet(X(\mathbb{C}), A)$between the étale cohomology of $X$ and the ordinary cohomology of $X(\mathbb{C})$.

Notice that on the other hand for instance if instead $X = Spec(k)$ is the spectrum of a field, then its étale cohomology coincides with the Galois cohomology of $k$. In this way étale cohomology interpolates between “topological” and “number theoretic” notions of cohomology.

]]>brief note *comparison theorem (étale cohomology)*