5. The statement
5.1. From subvarieties to cycles
With the class of a subvariety in hand, summing over the components of a cycle with their
multiplicities gives an additive map on integral cycles, and extension of scalars gives a
\mathbb Q-linear map on rational cycles. The evaluation formulas
below hold for all integer and rational coefficients.
def sheafCycleClassOnCycles (V : SmoothProjectiveComplexVariety) (d : ℕ)
[SmoothOfRelativeDimension d V.structureMap] (p : ℕ) :
codimensionCycleSubgroup V.scheme p →+ H^(2 * (p : ℤ))(V.over; ℚ) :=
cycleClassOnCyclesOfComponents (cycleComponentSheafClass V.over (d := d))
#check AlgebraicGeometry.ComplexPoint.sheafCycleClassOnCycles_single
def rationalSheafCycleClassOnCycles
(V : SmoothProjectiveComplexVariety) (d : ℕ)
[SmoothOfRelativeDimension d V.structureMap] (p : ℕ) :
TensorProduct ℤ ℚ (codimensionCycleSubgroup V.scheme p) →ₗ[ℚ]
H^(2 * (p : ℤ))(V.over; ℚ) :=
TensorProduct.AlgebraTensorModule.lift (sheafCycleClassRationalExtensionBilinear V d p)
#check AlgebraicGeometry.ComplexPoint.rationalSheafCycleClassOnCycles_tmul_single
These maps take a SmoothProjectiveComplexVariety, a scheme with its structure morphism to
\operatorname{Spec}\mathbb C, together with a natural number d and an instance saying
that the structure morphism is smooth of relative dimension d. The construction of the
class of a subvariety needs that dimension. For a smooth integral complex scheme the instance
holds at dim X.left, so a caller supplies dim X.left and typeclass search finds the
certificate.
algebraicCycleClassSpan, defined next, evaluates each class at dim X.left directly,
so the statement mentions the scheme and its structure morphism alone.
5.2. The algebraic subspace
For every point x of coheight p in X.left, the construction of the previous
section gives a class
\operatorname{cl}_X(\overline{\{x\}})\in H^{2p}(X;\mathbb Q).
The algebraic subspace is the rational span of these classes:
A^p(X)=\sum_{\operatorname{coht}(x)=p}
\mathbb Q\,\operatorname{cl}_X(\overline{\{x\}}).
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}
#check AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_mem_algebraicCycleClassSpan
In Lean the span is the supremum, over all points x and all proofs hx of
coheight x = p, of the line spanned by
cycleComponentSheafClass X x (d := dim X.left) hx, where the named argument fixes the
dimension at dim X.left.
5.3. The proposition
Here is the full statement, as declared in HodgeConjecture/Statement.lean. The copy shown here
is elaborated when the site is built, and the build checks that it is definitionally equal to the
declaration in the repository.
def HodgeConjecture : Prop :=
∀ (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (p : ℕ),
Hdg^p(ℚ; X) ≤ algebraicCycleClassSpan X p
It quantifies over a scheme X over \mathbb C that is integral with smooth and projective
structure morphism, and over a natural number p. The conclusion is the inclusion of subspaces
\operatorname{Hdg}^p(X;\mathbb Q)\le A^p(X):
every rational Hodge class of degree 2p is a rational linear combination of classes of
algebraic subvarieties of codimension p. This is the conjecture as Deligne states it,
pp. 45–46. The reverse
inclusion, that every algebraic class is a Hodge class, is a theorem that has not yet been
formalized, so the formulation as an equality \operatorname{Hdg}^p(X;\mathbb Q)=A^p(X) is not
yet available.
5.4. What the repository proves about the statement
The conjecture is stated, not proved. Two of its cases are proved outright.
The easy case is p>\dim X. A smooth variety has no point of coheight above its dimension, so
the span is \bot; and F^p vanishes there, so the Hodge classes are \bot too. The
inclusion holds because both sides are zero. It settles nothing about the conjecture, but it does
check that the two sides degenerate together, which a mismatch in the degree conventions would
break.
#check AlgebraicGeometry.ComplexPoint.hodgeClasses_eq_bot_of_lt
#check AlgebraicGeometry.ComplexPoint.algebraicCycleClassSpan_eq_bot_of_lt
Codimension zero is the substantial one. Both sides are computed, and they agree:
\operatorname{Hdg}^0(X;\mathbb Q)=A^0(X)=H^0(X;\mathbb Q).
#check AlgebraicGeometry.ComplexPoint.rationalHodgeClasses_zero_eq_algebraicCycleClassSpan
The left-hand side is everything, because F^0 is; that is the sanity check of
Hodge classes. The right-hand side is the line on a single class, that of
the generic point of X.left, since on an integral scheme no other point has coheight zero.
That line is all of H^0(X;\mathbb Q) for two reasons: the analytification of a smooth integral
complex scheme is connected, so H^0 is itself a line, and the class is nonzero. Connectedness
is proved here, from Noether normalization and a local étale chart, rather than assumed.
#check AlgebraicGeometry.ComplexPoint.hodgeClasses_zero_eq_top
#check AlgebraicGeometry.ComplexPoint.connectedSpace
#check AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_genericPoint_ne_zero
The nonvanishing is the part that tests the construction. Its proof runs the chain of
The class of a subvariety backwards: the normalized local section
is nonzero at any complex point of the smooth locus, the two normalization comparisons are
isomorphisms, and forgetting support is injective here because the generic component is supported
on all of X(\mathbb C). So the construction does not return zero, at least for this one
subvariety, on a variety of any dimension.
For a component of positive codimension the same chain stops at the last step. The normalized section is still nonzero, for every component:
#check AlgebraicGeometry.ComplexPoint.cycleComponentSmoothSupportCoclassSection_ne_zero
but forgetting support need not be injective on H^{2p}_Z(X;\mathbb Q), and showing that it is
on the fundamental-class line is cohomological purity, which is open; see
Scope and status. Until it is settled, A^p(X) is generated by classes
not yet known to be nonzero, so it could be smaller than the classical right-hand side, making
the statement stronger than the conjecture rather than weaker.
5.5. Reading the source
The shortest route through the implementation is:
-
HodgeConjecture/Statement.lean, the statement; -
HodgeConjecture/Definitions/AlgebraicGeometry/Hodge/Filtration.lean, cohomology and the Hodge filtration; -
HodgeConjecture/Lemmas/AlgebraicGeometry/Cohomology/WithSupport.lean, the mapping-cone model of cohomology with support; -
HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/Component/SmoothSupportCoclassSection.lean, the class on the smooth locus; -
HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/Component/SupportExtension.lean, its extension across the singular locus; -
HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/Component/SheafClass.lean, the class of a subvariety; -
HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/ClassSpan.lean, the span the statement compares against; -
Other/AlgebraicGeometry/SheafCycleClass.lean, the maps on cycles; -
Other/AlgebraicGeometry/CodimensionZeroClassComparison.leanandCodimensionZeroCoclassNonvanishing.lean, the codimension-zero case.
Other/AlgebraicGeometry/ComplexSheafBorelMoore.lean and its rational comparison are not on this
route. They build Borel–Moore homology of the pair Z\subset X and its duality with cohomology
with support; both live in Other/, so the import check that guards
HodgeConjecture/Statement.lean guarantees the statement does not reach them.
Things to keep track of while reading: integer versus natural-number degrees, real versus complex dimension, whether a class has been normalized, whether its support has been forgotten, and whether a class is supported or ordinary.