Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2013
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2013

    added a few more lines as such:


    Specifically, let AA be either of

    (but not for instance the integers themselves).

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

    H (X et,A)H (X(),A) H^\bullet(X_{et}, A) \simeq H^\bullet(X(\mathbb{C}), A)

    between the étale cohomology of XX and the ordinary cohomology of X()X(\mathbb{C}).

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

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 22nd 2013

    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.

    • CommentRowNumber4.
    • CommentAuthorZhen Lin
    • CommentTimeNov 22nd 2013

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

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2013
    • (edited Nov 22nd 2013)

    @David,

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

    Also the real numbers have been formalized in HoTT, in

    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?

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2013

    @Zhen Lin,

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