1. Overview
The conjecture concerns a smooth projective variety over \mathbb C. In Lean such a variety is an
object X of the over category Over (Spec ↧ℂ): a scheme X.left together with
its structure morphism X.hom, a morphism X.left ⟶ Spec ↧ℂ. The hypotheses are the
instance arguments IsIntegral X.left, Smooth X.hom and IsProjective X.hom.
The over category, the spectrum, integral schemes and smooth morphisms are Mathlib's;
projectivity and the complex points of X are defined in the repository, see
The variety and its complex points.
A codimension is a natural number p, while cohomological degrees are integers, so the class
of a codimension-p cycle lives in degree 2 * (p : ℤ); the coercion is visible in the
types below.
The statement is a single proposition, comparing two subspaces of rational cohomology. Here it is
as declared in HodgeConjecture/Statement.lean:
def HodgeConjecture : Prop :=
∀ (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (p : ℕ),
Hdg^p(ℚ; X) ≤ algebraicCycleClassSpan X p
The two subspaces are the rational Hodge classes and the algebraic subspace. Their definitions, whose ingredients the following sections explain, read:
def hodgeClasses (K : Type) [Field K] [Algebra K ℂ] (X : Over (Spec ↧ℂ)) [IsIntegral X.left]
[Smooth X.hom] (p : ℕ) : Submodule K (H^(2 * p)(X; K)) :=
((hodgePiece X p p (2 * p)).restrictScalars K).comap
(fieldToDeRhamCohomologyLinear K X (2 * p))
def algebraicCycleClassSpan (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom]
[IsProjective X.hom] (p : ℕ) : Submodule ℚ (H^(2 * (p : ℤ))(X; ℚ)) :=
⨆ (x : X.left) (hx : coheight x = p),
Submodule.span ℚ {cycleComponentSheafClass X x (d := dim X.left) hx}
Mathematically it is the inclusion
\operatorname{Hdg}^p(X;\mathbb Q)
\subseteq
\langle \operatorname{cl}_X(Z)\mid Z\subseteq X\text{ irreducible},
\operatorname{codim}_X Z=p\rangle_{\mathbb Q}
of the rational Hodge classes of degree 2p in the rational span of the classes of the
irreducible subvarieties of codimension p.
1.1. The construction in outline
-
Form the space
X(\mathbb C)of complex points with its analytic topology, and the holomorphic de Rham complex\Omega_X^\bulleton it. Rational cohomologyH^n(X;\mathbb Q)and de Rham cohomologyH^n_{\mathrm{dR}}(X)are hypercohomology groups of sheaf complexes onX(\mathbb C), and the maps of complexes\underline{\mathbb Q}_X\to\underline{\mathbb C}_X\to\Omega_X^\bulletinduce a comparison map from the first to the second. -
Define
F^pH^n_{\mathrm{dR}}(X)as the image of the hypercohomology of the truncated complex\Omega_X^{\ge p}, transport complex conjugation to de Rham cohomology, and setH^{p,q}=F^p\cap\overline{F^q}. The Hodge classes\operatorname{Hdg}^p(X;\mathbb Q)are the rational classes of degree2pwhose image under the comparison map lies inH^{p,p}; over\mathbb Qthis is the same as lying inF^p. -
Represent an irreducible subvariety
Z\subseteq Xof codimensionpby its generic point, a point of the schemeX.leftof coheightp, and form the cohomology ofX(\mathbb C)with support inZ. -
On the smooth locus of
Z, the complex orientation of the normal directions singles out a generator of the cohomology with support inZin degree2p, locally in charts, and these local generators glue. -
Extend the resulting class uniquely across the singular locus of
Z, which has codimension at leastp+1, so that its cohomology with support vanishes in degrees2pand2p+1. Forgetting the support gives\operatorname{cl}_X(Z)\in H^{2p}(X;\mathbb Q). -
Extend
\operatorname{cl}_Xadditively to cycles and\mathbb Q-linearly to rational cycles. The statement itself uses only the span of the classes of individual subvarieties.
The guide follows this order: steps 1 and 2 are the subject of Hodge classes, step 3 of Cycles and cohomology with support, steps 4 and 5 of The class of a subvariety, and step 6 of The statement.
Everything happens in cohomology with support. Other/ also builds a Borel–Moore homology of the
pair Z\subset X and the duality that identifies the class above with a fundamental class, but
nothing in the statement passes through it, so this guide leaves it aside.
1.2. Scope and status
Everything that enters the statement is constructed. The class of a subvariety of any codimension, singular or not, is defined outright, with no hypotheses beyond the smoothness, projectivity, and integrality of the ambient variety that the statement itself assumes.
Two cases of the conjecture itself are proved, both unconditionally, and both in
Other/AlgebraicGeometry/.
-
Codimension zero. Every degree-zero class is a Hodge class, and the class of
Xitself spansH^0(X;\mathbb Q), so\operatorname{Hdg}^0(X;\mathbb Q)=A^0(X). The two inputs are that the analytification of a smooth integral complex scheme is connected and that the constructed class of the whole variety is nonzero; both are proved here. The second is the useful one: it shows that the construction of the class of a subvariety does not return zero, which is the way a statement of this shape can hold for the wrong reason. -
Above the dimension. For
p>\dim Xboth sides are\bot: there is no point of coheightp, and the Hodge classes vanish becauseF^pdoes. The inclusion is then vacuous, but it does check that the two sides degenerate in the same place.
See What the repository proves about the statement for the declarations.
Three classical facts about the construction are not formalized. None is needed to state the conjecture, but they are needed for the usual equivalent formulations, and the first is what stands between the two cases above and the general one.
-
Cohomological purity:
H^{2p}_Z(X;\mathbb Q)is the line on the fundamental class, so that forgetting support is injective on it and\operatorname{cl}_X(Z)\ne0for every subvarietyZ. The normalized local section the class is built from is proved nonzero for every component; purity is what would carry that through to ordinary cohomology. Without it the spanA^p(X)is not known to be as large as the classes generating it suggest. -
The class of a subvariety is a Hodge class:
\operatorname{cl}_X(Z)\in\operatorname{Hdg}^p(X;\mathbb Q). This is the reverse inclusion, and it is what would turn the statement into the usual equality. -
The comparison between constant-sheaf and singular cohomology is not known to commute with forgetting support.
1.3. Degree and support conventions
A subvariety Z of codimension p in a smooth variety X of dimension d has p complex
normal directions, so its class sits in the cohomological degree 2p that the complex
orientation of those directions can generate. This is the origin of the index
2 * (p : ℤ) throughout the code; the complementary index
2 * ((d - p : ℕ) : ℤ), the real dimension of Z, appears wherever a construction is
indexed by Z rather than by its codimension. A class with support in Z lies in
H_Z^{2p}(X;\mathbb Q); the map forgetSupport sends it to the ordinary group
H^{2p}(X;\mathbb Q), in which the conjecture is stated.