Topic: The Hodge Conjecture
Kevin Buzzard (Jul 18 2019 at 21:15):
@Patrick Massot @Sebastien Gouezel @Johan Commelin @Scott Morrison @Reid Barton how far away are we from stating the Hodge Conjecture in Lean? That would be a cool thing to do.
Sebastien Gouezel (Jul 18 2019 at 21:25):
Quite far I would say. I have smooth manifolds (over R or C or whatever) and their tangent bundles, but not its exterior powers. This shouldn't be hard (shouldn't be easy either, by the way). But there is no cohomology yet, no long exact sequences, no snake lemma, and so on. And I haven't done anything on submanifolds either (next step on my TODO list is the local inverse theorem).
Johan Commelin (Jul 19 2019 at 06:34):
Heh, I guess we could benefit from a library on homological algebra and sheaf cohomology first (-;
Johan Commelin (Jul 19 2019 at 06:35):
Also, do you want to assume a proof of the Hodge theorem, or do you want to prove it as well? Because I don't know cheap proofs there.
Last updated: May 06 2021 at 19:30 UTC