Mention etale cohomology

[kbuzzard]

Joel points out https://leanprover.zulipchat.com/#narrow/stream/416277-FLT/topic/Project.20public/near/437127055 that it's necessary for attaching Galois representations to the modular forms we're interested in (we need this construction for Hilbert modular forms of level 1 for a totally real field of even degree (which can be assumed to be greater than 2), and I see no way of doing this short of using Jacquet-Langlands to switch to a compact surface and analysing the H^2.