Proposal: Complexifications with a view towards Hodge theory

Stream: mathlib4

[Simone Melchiorre Chiarello]

Hi all.
I’ve been studying Lean 4 in my spare time and would like to start contributing to Mathlib. I’m following the contribution guidelines and trying to begin with a small, self-contained addition in an area I know reasonably well: complex geometry.

My long-term personal motivation would be to formalize parts of Hodge theory, eventually the Hodge decomposition

$H^k(X;\mathbb{C}) = \bigoplus_{p+q=k}H^{p,q}(X).$

but I’m fully aware this is far beyond a first contribution. The actual proposal I’m considering is much more modest.

A basic ingredient used throughout Hodge theory is the complexification of a real vector space and the extension of a real “complex structure” $J$ with $J^2 = -\mathrm{Id}$. I couldn’t find a dedicated API for this in Mathlib, and the older discussion #Is there code for X? > Complexification of a real vector space doesn’t seem to have led to integrated code (please correct me if I missed something).

As a first experiment, I put together a small development on my personal fork: https://github.com/lsqrl/mathlib4/pull/1/files. This was done thinking about tangent space of a manifold, but the lemmas are just linear algebra (check my questions below).

For now, this exercises just shows that whenever we have an endomorphism $J$ on a real vector space such that $J^2 = -I$, such endomorphism naturally extends to the complexification as a $\mathbb{C}$-linear map, and that it decomposes its complexification as $V \otimes \mathbb{C} = V_i \oplus V_{-i}$ in eigenspaces for the eigenvalues $i$ and $-i$, and that one is the complex conjugate of the other.

As this is my first non-trivial task in Mathlib, I'd like to ask some questions on this channel.

1. Does this look like a reasonable scope for a first Mathlib contribution?
2. Conceptually, this is linear algebra, but its main use (at least for me) is in complex/differential geometry. Would something like LinearAlgebra/Complex/Complexification be an appropriate home, or is there a better place?
3. There are many small “obvious” lemmas one could add about complexification and conjugation. From a Mathlib perspective, what’s a good balance between building a clean baseline API and keeping the contribution minimal and useful?

The code I have is vibe-coded, therefore it is rough and exploratory, but I’ll definitely improve it once I understand better what shape would be most appropriate for Mathlib.

Thanks very much for any feedback, and happy holidays!

[Thomas Browning]

If it's possible to extract the purely linear-algebraic notion of a complex structure on a single vector space, then that should live in LinearAlgebra. But once you start introducing manifolds into the picture, then it should live in Geometry/Manifold.

[Johan Commelin]

Hi @Simone Melchiorre Chiarello, it would be marvelous to get some Hodge theory into Mathlib.

Concerning #Is there code for X? > Complexification of a real vector space : as pointed out there, for constructing the complexification, we have the tensor product available in Mathlib.

But it is probably useful to have a dedicated API for the following setting: an extension of fields $L/K$ (or maybe just two rings, one an algebra over the other) and an $L$-vector space $V$ that is endowed with a $K$-structure: a $K$-subspace $V_0$ such that the natural map $L \otimes_K V_0 \to V$ is an isomorphism.

Maybe we want even more specialized API for the $\mathbb{C}/\R$ setting, I don't know yet. Some of what you write generalizes to $L/K$. I think, if $L$ is the splitting field over $K$ of some polynomial $f$ with roots $\alpha_1, \dots, \alpha_n$, then you get a decomposition of the $L$-space into $\alpha_i$-eigenspaces.

My gut instinct is that if we invest in complexification and complex structures, then we might as well aim at this more general setting. Are you familiar with this bit of theory?

[Johan Commelin]

There is also #maths > Hodge star operator which you might enjoy.

[Kevin Buzzard]

As it happens I'm right now wishing we had a theory of lattices in vector spaces over number fields (I need a free $\mathcal{O}_K$-submodule of a finite-dimensional $K$-vector space, $K$ a number field)

[Kevin Buzzard]

But we already have docs#IsTensorProduct so maybe this is enough?

[Andrew Yang]

Probably docs#IsBaseChange fits better, but we hardly have any API on it.

[Andrew Yang]

The docstring of that is borderline unreadable but basically (V₀ : Submodule K V) : IsBaseChange L V₀.subtype is "a $K$-subspace $V_0$ such that the natural map $L \otimes_K V_0 \to V$ is an isomorphism".

[Simone Melchiorre Chiarello]

@Johan Commelin I have nothing against developing the theory for general $L/K$ extension. I am totally not familiar with such a theory, but it seems legit to prove analogous statements as long as $L$ is Galois and finite: it would ensure that $J$ whose characteristic polynomial is irreducible and splits in $L$ is diagonalizable. Action of the Galois group naturally extends to $V\otimes_K L$ and it would permute eigenspaces. If it's not separable I would need to think more, but my gut feeling is the structure would be less usable: we wouldn't have any non-trivial automorphism acting on $L$ fixing $K$ (no "conjugate") and no canonical splitting but just a filtration following the nilpotency of $J - \lambda I$.

@Kevin Buzzard the lattice theory path seems very interesting even for Hodge theory, since at some point one may want to discuss algebraic cycles $H^{2k}(X;\mathbb{Z})$ of a smooth complex projective variety and maybe the Hodge conjecture. Also totally for it.

At the beginning, my rationale was not just "complexification", which as pointed out is just one and just a tensor product, but rather having an API for complex structures J and the structures they induce. Such structure can be plenty even on a single underlying smooth manifold, and they induce different Hodge structures. So I thought the theory was "rich enough" to just start with $\mathbb{C}$ and $J^2=-I$.

I remind that this is my first serious exercise in Mathlib, so for me basically any project leading to a contribution is good. Also, my current goal at least short-term is not to write the entire Hodge theory API in Mathlib but just to make a useful contribution in that direction. Of course if any particular project met collaboration or help, that would significantly increase my motivation! :)

Thanks everybody for your answers!

[Joël Riou]

In Hodge II https://www.numdam.org/item/PMIHES_1971__40__5_0.pdf Deligne defines the notion of n-opposed filtrations (1.2) on a filtered object (in an abelian category). I would think it would be interesting to develop this notion, as this is the basis for the definition of (pure) Hodge structures.

[Simone Melchiorre Chiarello]

Thanks @Joël Riou for your answer. This actually has triggered some literature research on my side. Following also the other suggestions in this thread, it seems to be more interesting for the community to define pure and mixed Hodge structures, and proving theorems on them directly. The geometric bridge (Hodge theorem: the Dolbeault cohomology of a compact Kahler manifold admits a Hodge structure, and the statements about the non-compact case with mixed structures) can be put aside for now and would become more natural once the Hodge API is established.

In order to start, I was thinking of following the classical textbook Peters C.A., Steenbrink J.H. - Mixed Hodge Structures, in particular Chapter 2 is fully algebraic and has the good plus of covering the case of number fields. This is not as geometric as Voisin's book, so might meet the indications of this thread more closely.