Hodge decomposition: $H^k(X,\mathbb{C}) = \bigoplus_{p+q=k} H^{p,q}(X)$ for a projective non-singular variety

Read-back of hodge_decomposition

Statement in one sentence. For every natural numbers $N, n, k$, every "projective variety" $X$ in the sense defined below (a set of homogeneous polynomials in $N+1$ complex variables), assuming $X$ is "nonsingular of dimension $n$" in the sense defined below, and every element $c$ of the $k$-th "cohomology group" $H^k(X)$ defined below, there is exactly one function $f$ from the index set $\{0,1,\dots,k\}$ to $H^k(X)$ such that

$$\bigl(\forall p\in\{0,\dots,k\}:\ f_p \text{ "has type } (p,\,k-p)\text{"}\bigr)\quad\text{and}\quad c=\sum_{p=0}^{k} f_p .$$

"Exactly one" means: such an $f$ exists, and any $g:\{0,\dots,k\}\to H^k(X)$ satisfying the same two conditions is equal to $f$ as a function (i.e. $g_p=f_p$ for every $p$). Here $p$ ranges over $\{0,\dots,k\}$, so $k-p$ is an ordinary subtraction with $0\le k-p\le k$; the natural-number truncation of subtraction never actually fires, and every pair $(p,k-p)$ that appears satisfies $p+(k-p)=k$. The sum is taken in the abelian group $H^k(X)$ (a $\mathbb C$-vector space). Everything in quotes is a bespoke definition, expanded below.

---

1. Ambient spaces and the operators $J_P$, $z\cdot_P$

• Coordinates. $V:=\mathbb C^{N+1}$ (functions $\{0,\dots,N\}\to\mathbb C$).
• Ambient matrix space. $M:=$ the space of $(N+1)\times(N+1)$ complex matrices, given the Hilbert–Schmidt (Euclidean $\ell^2$) norm. It is a complex Hilbert space of complex dimension $(N+1)^2$; it is also regarded as a real vector space of real dimension $2(N+1)^2$.
• The map $\pi:V\to M$.

$$\pi(v)_{ij}=\frac{v_i\,\overline{v_j}}{\sum_{l}|v_l|^2}\qquad(\text{the denominator is a real number, coerced to }\mathbb C).$$

For $v\neq0$ this is the rank-one Hermitian projection matrix onto the line $\mathbb Cv$, and $\pi(\lambda v)=\pi(v)$ for $\lambda\in\mathbb C^\times$. For $v=0$ the division is by $0$, which in Lean's $\mathbb C$ yields $0$, so $\pi(0)=0$ (the zero matrix).

• The operator $J_P$. For $P,A\in M$,

$$J_P(A):=i\,(AP-PA)=i\,[A,P],\qquad\text{entrywise } (J_P A)_{ij}=i\sum_{l}\bigl(A_{il}P_{lj}-P_{il}A_{lj}\bigr).$$

$J_P$ is $\mathbb C$-linear in $A$ for every $P$; no property such as $J_P^2=-1$ is assumed or asserted anywhere.

• The "twisted scalar multiplication" $z\cdot_P A$. For $P,A\in M$ and $z\in\mathbb C$,

$$z\cdot_P A:=(\operatorname{Re}z)\,A+(\operatorname{Im}z)\,J_P(A)=(\operatorname{Re}z)\,A+(\operatorname{Im}z)\,i[A,P].$$

For real $z$ this is ordinary scaling $zA$; for non-real $z$ it is not the complex scalar product $zA$ of the matrix $A$ in general.

2. "Projective variety", cone, points, tangent spaces, nonsingularity

• A projective variety $X$ (in $\mathbb P^N$) is a set $E_X$ of polynomials in $N+1$ complex variables such that every $Q\in E_X$ is homogeneous of some degree $d\in\mathbb N$ (depending on $Q$). Degree $0$ is allowed, so $E_X$ may contain nonzero constants; the zero polynomial is homogeneous of every degree and may also belong to $E_X$; $E_X$ may be empty.
• The cone. $C_X:=\{v\in V : v\neq0 \text{ and } Q(v)=0\ \forall Q\in E_X\}\subseteq V\setminus\{0\}$.
• The point set. $\mathrm{pts}(X):=\pi(C_X)\subseteq M$, the set of rank-one projections onto lines through points of the cone. If $C_X=\varnothing$ (e.g. $E_X$ contains a nonzero constant) then $\mathrm{pts}(X)=\varnothing$. If $E_X=\varnothing$ then $C_X=V\setminus\{0\}$.
• The vanishing ideal. $I_X:=\{Q : Q(v)=0\ \forall v\in C_X\}$, all polynomials (homogeneous or not) vanishing on the cone. If $C_X=\varnothing$, $I_X$ is the set of all polynomials.
• The Zariski tangent space of the cone at $v\in V$ (defined for every $v$, not only $v\in C_X$):

$$T_v:=\bigcap_{Q\in I_X}\ker\bigl(dQ_v\bigr)\subseteq V,\qquad dQ_v(u)=\sum_{i=0}^{N}\frac{\partial Q}{\partial x_i}(v)\,u_i,$$

a complex-linear subspace of $V=\mathbb C^{N+1}$. (If $C_X=\varnothing$ then, since all coordinate functions lie in $I_X$, $T_v=\{0\}$ for every $v$.)

• The hypothesis "$X$ is nonsingular of dimension $n$" (the hypothesis $h_X$ of the theorem) is literally

$$\forall v\in C_X:\quad \dim_{\mathbb C} T_v = n+1 .$$

This is a statement about the affine cone: the complex dimension of the tangent space to the cone at each nonzero cone point is $n+1$. Nothing is assumed about irreducibility, non-emptiness, or the relation between $n$ and $N$. If $C_X=\varnothing$, this hypothesis holds vacuously for every $n$.

• The real tangent space of $\mathrm{pts}(X)$ at $P\in M$ (defined for every $P\in M$):

$$\mathcal T_P:=\sum_{\substack{v\in C_X\\ \pi(v)=P}} \bigl(D\pi_v\bigr)\bigl(T_v\bigr)\ \subseteq M,$$

the real-linear span (supremum of real subspaces) over all cone points $v$ lying over $P$ of the image of $T_v$ (regarded as a real subspace of $V$) under the real Fréchet derivative $D\pi_v:V\to M$ of $\pi$ at $v$. Since every such $v$ is nonzero, $\pi$ is genuinely differentiable there. If $P\notin\mathrm{pts}(X)$ the family is empty and $\mathcal T_P=\{0\}$.

3. Forms, smoothness, the exterior derivative, closed and exact forms, cohomology

• A $k$-form is any function $\omega:M\to \operatorname{Alt}^k_{\mathbb R}(M;\mathbb C)$, where $\operatorname{Alt}^k_{\mathbb R}(M;\mathbb C)$ is the space of continuous real-multilinear alternating maps $M^k\to\mathbb C$. No regularity is built into the notion of form. Forms are $\mathbb C$-valued, hence form a $\mathbb C$-vector space $\Omega^k$ (scalars act on the value). For $k=0$, $\operatorname{Alt}^0\cong\mathbb C$, so a $0$-form is just a function $M\to\mathbb C$.
• Smoothness "$C^\infty$". The symbol $\infty$ used in the definitions denotes the smoothness order "infinitely differentiable" (all finite orders), not real-analytic. "$\omega$ is $C^\infty$" means $\omega$ is infinitely real-differentiable on all of $M$ (the entire matrix space, not only on or near $\mathrm{pts}(X)$), as a map from the finite-dimensional real space $M$ into the Banach space $\operatorname{Alt}^k_{\mathbb R}(M;\mathbb C)$.
• Exterior derivative. $d\omega$ denotes Mathlib's exterior derivative of $\omega$: a $(k+1)$-form obtained pointwise by alternatizing the real Fréchet derivative of $\omega$ (at any point where $\omega$ is not differentiable the derivative is taken to be $0$, so $d\omega$ is a total function with junk value $0$ there). In the definitions below $d$ is only ever applied to forms that are required to be $C^\infty$, so this junk convention is not exercised.
• "$\eta$ vanishes on $X$" (for a $k$-form $\eta$):

$$\forall P\in\mathrm{pts}(X),\ \forall (v_0,\dots,v_{k-1})\in M^k:\ \bigl(\forall i,\ v_i\in\mathcal T_P\bigr)\Rightarrow \eta(P)(v_0,\dots,v_{k-1})=0 .$$

Only points of $\mathrm{pts}(X)$ and only tangent directions $\mathcal T_P$ are tested. For $k=0$ this reads $\eta(P)=0$ for all $P\in\mathrm{pts}(X)$. If $\mathrm{pts}(X)=\varnothing$ every form vanishes on $X$.

• $\omega$ is a closed $k$-form: $\omega$ is $C^\infty$ on $M$ and $d\omega$ vanishes on $X$ (in the sense just defined). Nothing is required of $d\omega$ away from $\mathrm{pts}(X)$ or in non-tangent directions.
• $\omega$ is an exact $k$-form:
• $k=0$: $\omega$ is $C^\infty$ on $M$ and $\omega$ vanishes on $X$ (i.e. $\omega(P)=0$ for all $P\in\mathrm{pts}(X)$);
• $k\ge1$: $\omega$ is $C^\infty$ on $M$ and there exists a $(k-1)$-form $\alpha$, $C^\infty$ on $M$, such that $\omega-d\alpha$ vanishes on $X$.
• $Z^k(X)$ := the $\mathbb C$-linear span, inside $\Omega^k$, of the set of closed $k$-forms. $B^k(X)$ := the $\mathbb C$-linear span, inside $\Omega^k$, of the set of exact $k$-forms. (Spans are taken formally; membership in $Z^k(X)$ or $B^k(X)$ means being a finite $\mathbb C$-linear combination of closed, resp. exact, forms.) It is not part of the definitions that $B^k(X)\subseteq Z^k(X)$.
• $H^k(X)$ := the image of $Z^k(X)$ under the quotient map $\Omega^k\to\Omega^k/B^k(X)$; equivalently $Z^k(X)/\bigl(Z^k(X)\cap B^k(X)\bigr)$, a $\mathbb C$-vector space. Its elements are the "cohomology classes".
• $[\omega]$ for $\omega\in Z^k(X)$ := the class of $\omega$ in $H^k(X)$.

4. "Type $(p,q)$"

• A $k$-form $\omega$ has type $(p,q)$ (for $p,q\in\mathbb N$) iff

$$\forall P\in\mathrm{pts}(X),\ \forall (v_0,\dots,v_{k-1})\in M^k \text{ with all } v_i\in\mathcal T_P,\ \forall z\in\mathbb C:\quad \omega(P)\bigl(z\cdot_P v_0,\dots,z\cdot_P v_{k-1}\bigr)=z^{p}\,\overline{z}^{\,q}\;\omega(P)(v_0,\dots,v_{k-1}),$$

where $z\cdot_P v_i=(\operatorname{Re}z)v_i+(\operatorname{Im}z)\,i[v_i,P]$. The vectors $z\cdot_P v_i$ are not required to lie in $\mathcal T_P$; $\omega(P)$ is evaluated on them as elements of $M$. The condition is tested only at points of $\mathrm{pts}(X)$ and only for tangent inputs.

• A class $c\in H^k(X)$ has type $(p,q)$ iff there exists some $\omega\in Z^k(X)$ with $[\omega]=c$ and $\omega$ has type $(p,q)$. It is an existence statement about one representative; other representatives of $c$ need not have type $(p,q)$.

5. The theorem, fully expanded

Let $N,n,k\in\mathbb N$ be arbitrary, let $X$ be any set $E_X$ of homogeneous polynomials in $N+1$ complex variables, and suppose that for every nonzero common zero $v$ of $E_X$ the complex dimension of $T_v=\bigcap_{Q\in I_X}\ker dQ_v$ equals $n+1$. Let $c\in H^k(X)$. Then there exists a unique tuple $(f_0,f_1,\dots,f_k)$ of elements of $H^k(X)$ such that:

1. for each $p\in\{0,\dots,k\}$ there is a form $\omega_p\in Z^k(X)$ (a $\mathbb C$-combination of $C^\infty$ forms on $M$ whose exterior derivatives vanish on tangent directions at points of $\mathrm{pts}(X)$) with $[\omega_p]=f_p$ and

$$\omega_p(P)\bigl(z\cdot_P v_0,\dots,z\cdot_P v_{k-1}\bigr)=z^{p}\,\overline{z}^{\,k-p}\,\omega_p(P)(v)\quad\text{for all }P\in\mathrm{pts}(X),\ v_i\in\mathcal T_P,\ z\in\mathbb C;$$

2. $c=f_0+f_1+\dots+f_k$ in $H^k(X)$.

Uniqueness is of the whole tuple: any other tuple $(g_0,\dots,g_k)$ satisfying 1 and 2 has $g_p=f_p$ for all $p$.

6. Edge and degenerate cases visible in the statement

• $k=0$. The index set is $\{0\}$, the tuple is a single class $f_0$, condition 2 forces $f_0=c$, and condition 1 asks that $c$ have type $(0,0)$. For $0$-forms the tuple $v$ is empty, so the type condition reads $\omega(P)=z^0\overline z^0\,\omega(P)=\omega(P)$, which holds for every $0$-form and every $z$ (including $z=0$, as $0^0=1$). Hence every $c\in H^0(X)$ has type $(0,0)$ via any representative, and the $k=0$ instance of the theorem holds trivially.
• Natural-number subtraction. Since $p\le k$, $k-p$ is never truncated; all pairs are $(p,k-p)$ with $p+q=k$.
• Type $(p,q)$ with $p+q\neq k$ (not used by the theorem, but relevant to what "type" means). For real $z$, $z\cdot_P v_i=zv_i$, so real $k$-multilinearity gives $\omega(P)(zv)=z^k\omega(P)(v)$, while the right side is $z^{p+q}\omega(P)(v)$; for $p+q\neq k$ and real $z\notin\{0,1\}$ (and $z\ne-1$ when parity permits) this forces $\omega(P)(v)=0$ for all tangent $v$ at all $P\in\mathrm{pts}(X)$. So a form of type $(p,q)$ with $p+q\ne k$ is one that vanishes on $X$. In the theorem itself $p+q=k$ always, so this degeneracy does not arise.
• $z=0$. For $k\ge1$ the left side is $\omega(P)(0,\dots,0)=0$; the right side is $0^p\,0^{\,k-p}\,\omega(P)(v)=0$ since at least one exponent is positive. No constraint is imposed.
• The zero class. The zero form has every type $(p,q)$ (both sides are $0$), so $0\in H^k(X)$ has type $(p,q)$ for all $p,q$. Consequently, the components $f_p$ are permitted to be $0$.
• Empty cone. If $E_X$ has no nonzero common zero (e.g. it contains a nonzero constant), then $\mathrm{pts}(X)=\varnothing$, the nonsingularity hypothesis holds vacuously for every $n$, every form vanishes on $X$, closed $=$ exact $=$ $C^\infty$, so $Z^k(X)=B^k(X)$ and $H^k(X)=\{0\}$; the theorem then asserts only that the zero tuple is the unique decomposition of $0$, which holds.
• Non-differentiable points. Forms are arbitrary functions on $M$; the exterior derivative is a total function taking the value $0$ where the form is not differentiable, but every place $d$ is applied in these definitions is guarded by a $C^\infty$-on-$M$ requirement. $\pi$ is not differentiable at $v=0$, but $\mathcal T_P$ only uses $D\pi_v$ at cone points $v\ne0$.
• Meaning of $\infty$. "Smooth" throughout means $C^\infty$ (all finite orders of real differentiability on the whole of $M$), not analytic.
• No further hypotheses. Nothing relates $n$ to $N$ or $k$ (e.g. $k>2n$ is allowed); $X$ need not be irreducible or nonempty; $N$ may be $0$ (then $V=\mathbb C$, $M=\mathbb C$, $\pi(v)=1$ for $v\ne0$).