The Hodge Conjecture Formalization

6. References🔗

Each entry points to the part of the source that develops a construction used in the formalization.

  • Pierre Deligne, The Hodge Conjecture, in The Millennium Prize Problems, Clay Mathematics Institute and American Mathematical Society, 2006, pp. 45–53. §1 (pp. 45–46): the Hodge filtration, the classes of algebraic cycles, Hodge classes, and the statement of the conjecture. P. 51: the truncated holomorphic de Rham complex F^p\Omega^\bullet_{\mathrm{hol}}.

  • The Stacks Project, §50.7, “The Hodge filtration”: F^pH^n_{\mathrm{dR}} as the image of the hypercohomology of the truncation \sigma_{\ge p}\Omega^\bullet.

  • The Stacks Project, §42.42, “Cycles of given codimension”: cycles as combinations of generic points.

  • The Stacks Project, §20.21, “Cohomology with support in a closed subset”: sections with support, their derived functors, and the long exact sequence.

  • Mark Goresky, Lecture Notes on Sheaves and Perverse Sheaves: §3.10 (p. 17), the de Rham complex as a resolution of the constant sheaf; §§7.14–7.15 (pp. 31–32), the exact sequence of a pair and the support triangle; §8.11 (p. 37), fundamental classes and Poincaré duality for pseudomanifolds.

  • John M. Lee, Introduction to Complex Manifolds, Proposition 1.49: the canonical orientation of a complex manifold, preserved by local biholomorphisms.

6.1. Where the constructions live🔗

  • HodgeConjecture/Definitions/AlgebraicGeometry/Hodge/HolomorphicDeRham.lean and Filtration.lean: the de Rham complex, hypercohomology, and the Hodge filtration;

  • Other/AlgebraicGeometry/CodimensionCycle.lean, HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/Support.lean, and HodgeConjecture/Lemmas/AlgebraicGeometry/Cohomology/WithSupport.lean: cycles, their supports, and cohomology with support;

  • HodgeConjecture/Definitions/AlgebraicGeometry/Cycle/Component/SmoothSupportCoclassSection.lean and SupportExtension.lean: the class on the smooth locus and 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 of those classes, which is the right-hand side of the statement;

  • Other/AlgebraicGeometry/SheafCycleClass.lean: the maps on cycles;

  • Other/AlgebraicGeometry/SmoothAnalytificationConnected.lean: connectedness of the analytification of a smooth integral complex scheme;

  • Other/AlgebraicGeometry/CodimensionZeroClassComparison.lean and CodimensionZeroCoclassNonvanishing.lean: nonvanishing of the class of the whole variety and the codimension-zero case of the conjecture;

  • HodgeConjecture/Lemmas/LinearAlgebra/HodgeStructure.lean: pure Hodge structures and the (p,p) criterion.