The Hodge Conjecture

Stream: maths

[Kevin Buzzard]

@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]

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]

Heh, I guess we could benefit from a library on homological algebra and sheaf cohomology first (-;

[Johan Commelin]

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.

[Will Sawin]

Can't one state "every rational cohomology class represented by a (p,p)-form is also represented by a Q-linear combination of subvarieties" without using the Hodge theorem itself?

[Johan Commelin]

Good point, that certainly works.

[Johan Commelin]

Still, I personally feel that "there exists a natural Hodge structure on the cohomology of algebraic varieties" is a moral prerequisite to the Hodge conjecture.