Hirzebruch-Riemann-Roch (Lecture XIV)

Disproved

CondC.hrr

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

chern-characterriemann-rochtodd-class

The fourth headline theorem, the Hirzebruch-Riemann-Roch formula of Lecture XIV: for a compact complex manifold X and a vector bundle V, the Euler characteristic chi(X, V) = the alternating sum of the dimensions of the cohomology groups equals the integral of the product of the Chern character of V with the Todd class of the tangent bundle, computed in Hodge cohomology. The milestone states the formula over the HRR world interface: if the Euler characteristic is additive on the K-group, the Chern character is a unital ring homomorphism, and the integral is additive, then the Euler characteristic of every class of the K-group is the integral of the product of its Chern character with the Todd class. In the paper the formula is deduced from Grothendieck-Riemann-Roch (Theorem 14.9) together with the projective bundle formula; that deduction is the proposed work of the goal.

Formalization Note The K-group, the Hodge cohomology, the Chern character, the Todd class, the integral, and the Euler characteristic are abstract interface data; constructing them for compact complex manifolds and verifying the hypotheses is part of the proposed work.

Preamble

import Mathlib
import Definitions.Def_CondC_liq
import Definitions.Def_CondC_geo

Formal statement

namespace CondC

/-!  The goal: the Hirzebruch-Riemann-Roch theorem (Lecture XIV). In an HRR
world - a K-group with its operations, Hodge cohomology, the Chern
character, the Todd class, the integration functional, and the Euler
characteristic - if the Euler characteristic is additive, the Chern
character is a unital ring homomorphism, and the integral is additive, then
for every class v of the K-group the Euler characteristic is the integral of
the product of the Chern character of v with the Todd class:
chi(X, V) = the integral of ch(V) Td(T_X), the HRR formula of Lecture XIV.
The Grothendieck-Riemann-Roch theorem (Theorem 14.9) and the projective
bundle formula that imply it are the proposed work of the mission.  -/
theorem hrr : ∀ w : HRRWorld,
    (∀ x y : w.K, w.chi (w.addK x y) = w.chi x + w.chi y) →
    (∀ x y : w.K, w.ch (w.addK x y) = w.addH (w.ch x) (w.ch y)) →
    (∀ x y : w.K, w.ch (w.mulK x y) = w.mulH (w.ch x) (w.ch y)) →
    (w.ch w.oneK = w.oneH) →
    (∀ x y : w.Hdg, w.integral (w.addH x y) = w.integral x + w.integral y) →
    ∀ v : w.K, w.chi v = w.integral (w.mulH (w.ch v) (w.td)) := by sorry

end CondC

Source

D. Clausen, P. Scholze, Condensed Mathematics and Complex Geometry, lecture notes (May 2026 version), Lectures I and XIV (the Hirzebruch-Riemann-Roch formula of page 127, via Theorem 14.9).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in every HRR world whose Euler characteristic is additive on the K-group, whose Chern character is additive and multiplicative and sends the unit to the unit, and whose integral is additive, the Euler characteristic of every class of the K-group equals the integral of the product of the Chern character of that class with the Todd class. No other hypotheses appear.

View graph