2.1. The variety and its complex points🔗

We begin with the definition of a projective morphism of schemes.

A point of a scheme over \operatorname{Spec}R with values in R is a morphism over \operatorname{Spec}R; the complex points are the case R=\mathbb C. Each has an underlying scheme point.

The analytic topology is glued from affine charts. Over an affine open U, evaluating regular functions embeds the points above U into \operatorname{Hom}(\Gamma(U),R) with the topology of pointwise convergence, and the analytic topology is the finest topology for which all these charts are continuous. It is generated by the sets on which a local regular function takes values in a prescribed open subset of R; for R=\mathbb C this is the usual analytic topology.

The dimension of X is the Krull dimension of its underlying space, as a natural number.

2.2. The holomorphic de Rham complex🔗

Let X be a smooth complex scheme. The formalization works on the space X(\mathbb C) of its complex points with the analytic topology. Holomorphic differential forms on this space are first assembled into presheaves, and exterior differentiation makes them a complex of presheaves

\mathcal O_X \xrightarrow{d} \Omega_X^1 \xrightarrow{d} \Omega_X^2 \xrightarrow{d}\cdots.

Sheafifying degree by degree gives the holomorphic de Rham complex, indexed by the natural numbers: its terms are the sheaves of holomorphic forms and its differentials the exterior derivatives, both constructed in HodgeConjecture/Definitions/AlgebraicGeometry/Hodge/HolomorphicDeRham.lean.

Extending by zero to the integers gives the version used from now on, because the shifts used later act on \mathbb Z-indexed complexes.

Constant functions give a morphism to the de Rham complex from the constant sheaf \underline{\mathbb C}_X, placed in degree zero.

The instance below is the holomorphic Poincaré lemma:

It says that, on stalks, a closed holomorphic form of positive degree is exact, and the closed holomorphic functions are the locally constant ones, so

\underline{\mathbb C}_X \longrightarrow \Omega_X^\bullet

is a quasi-isomorphism. This is the analytic de Rham theorem in the form used below. Goresky's notes, §3.10, explain how the Poincaré lemma exhibits the de Rham complex as a resolution of the constant sheaf and thereby computes its cohomology.

2.3. Cohomology as morphisms in the derived category🔗

For a complex of sheaves K^\bullet on X(\mathbb C), hypercohomology is defined as a group of morphisms in the derived category,

\mathbb H^n(X,K^\bullet) =\operatorname{Hom}_{D(X)}(\underline{\mathbb Z}_X,K^\bullet[n]),

where \underline{\mathbb Z}_X is the constant sheaf in degree zero. The derived category is never constructed: Mathlib's Localization.SmallShiftedHom provides these morphism groups in the localization of complexes at quasi-isomorphisms without choosing a model for it. Rational cohomology and de Rham cohomology are the cases K^\bullet=\underline{\mathbb Q}_X and K^\bullet=\Omega_X^\bullet.

Cohomology with coefficients in a field K is the case of the constant sheaf K, and it is written with the notation H^n(X;K):

The comparison map H^n(X;\mathbb Q)\to H^n_{\mathrm{dR}}(X) is induced by the composite \underline{\mathbb Q}_X\to\underline{\mathbb C}_X\to\Omega_X^\bullet. It is \mathbb Q-linear and injective; injectivity combines the quasi-isomorphism above with the injectivity of extending scalars from \mathbb Q to \mathbb C. Nothing more is needed, since Hodge classes are defined as a preimage along this map.

2.4. The Hodge filtration🔗

The Hodge filtration comes from the stupid truncation of the de Rham complex,

F^p\Omega_X^\bullet=\sigma_{\ge p}\Omega_X^\bullet =[0\to\cdots\to0\to\Omega_X^p\to\Omega_X^{p+1}\to\cdots].

Its inclusion into \Omega_X^\bullet induces a map on hypercohomology, and F^pH^n_{\mathrm{dR}}(X) is the image of that map. This is the standard definition; compare the Stacks Project, §50.7, and Deligne's article, p. 51, where the same truncated complex appears.

The image is a priori an additive subgroup. Compatibility with complex scalars is proved, and hodgeFiltrationComplexSubmodule bundles the image as a \mathbb C-subspace, which restricts to a subspace over any coefficient field contained in \mathbb C. Two sanity checks are also proved: F^0 is all of H^n_{\mathrm{dR}}(X), and F^p=0 for p>\dim X. Both are used later — the first is what makes every degree-zero class a Hodge class, the second is what makes the conjecture vacuous above the dimension.

2.5. Complex conjugation and the Hodge pieces🔗

The Hodge pieces H^{p,q} are defined by the identity

H^{p,q}=F^p\cap\overline{F^q},

which holds in any pure Hodge structure and needs no Hodge decomposition theorem. Complex conjugation is not \mathbb C-linear, so it does not act on the holomorphic de Rham complex. It acts on the constant sheaf \underline{\mathbb C}_X by conjugating coefficients, and it is transported to de Rham cohomology across the comparison isomorphism of the first subsection.

The result is an involution and is conjugate-linear, so it can be bundled as a semilinear map; \overline{F^q} is then the preimage of F^q under it.

The degree n is an independent index, as for the filtration; when p+q=n this is the usual (p,q) piece.

2.6. Hodge classes🔗

The Hodge classes of degree 2p with coefficients in a field K\subseteq\mathbb C are the classes whose de Rham image lies in the (p,p) piece:

\operatorname{Hdg}^p(X;K) =\{\alpha\in H^{2p}(X;K):\alpha_{\mathrm{dR}}\in H^{p,p}\}.

In Lean this is the preimage of hodgePiece under the comparison map, and the notation Hdg^p(ℚ; X) abbreviates the case K=\mathbb Q.

The cohomology of X is not equipped with a pure Hodge structure in the formalization; that would require the Hodge decomposition. The (p,p) piece is instead defined directly by the formula above, which is why the conjugation had to be constructed.

The two sanity checks on the filtration pass to the Hodge classes: every degree-zero class is a Hodge class, and there are none above the dimension. These are the two ends of the conjecture that the repository settles; see What the repository proves about the statement.

2.7. Why the filtration alone suffices over the rationals🔗

Deligne states the conjecture with the condition \alpha_{\mathrm{dR}}\in F^p alone, p. 46, and over \mathbb Q the two conditions agree. When complex conjugation fixes K, a K-rational class is its own conjugate, so lying in F^p already forces lying in \overline{F^p}. The first lemma below proves this for any such K; the second specializes it to \mathbb Q, the coefficient field of the conjecture.

The same argument in an abstract pure Hodge structure of weight 2p is the lemma below, from HodgeConjecture/Lemmas/LinearAlgebra/HodgeStructure.lean: conjugation fixes rational vectors and exchanges H^{a,b} with H^{b,a}, so a rational vector in F^p=\bigoplus_{a\ge p}H^{a,2p-a} also lies in \overline{F^p}=\bigoplus_{b\ge p}H^{2p-b,b}, and the only summand common to both is H^{p,p}.

The conjugation condition cannot be dropped for other coefficient fields. Let E be the elliptic curve \mathbb C/(\mathbb Z+\mathbb Z i). The periods of dz are 1 and i, so dz is a \mathbb Q(i)-rational class spanning H^{1,0}(E), and on E\times E the class \mathrm{pr}_1^*dz\wedge\mathrm{pr}_2^*dz is \mathbb Q(i)-rational of type (2,0). It lies in F^1H^2 but not in H^{1,1}, so a definition by F^p alone would count it as a Hodge class of codimension one, although no algebraic class can reach it.