mathlib3 documentation

geometry.manifold.complex

Holomorphic functions on complex manifolds #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Thanks to the rigidity of complex-differentiability compared to real-differentiability, there are many results about complex manifolds with no analogue for manifolds over a general normed field. For now, this file contains just two (closely related) such results:

Main results #

TODO #

There is a whole theory to develop here. Maybe a next step would be to develop a theory of holomorphic vector/line bundles, including:

Another direction would be to develop the relationship with sheaf theory, building the sheaves of holomorphic and meromorphic functions on a complex manifold and proving algebraic results about the stalks, such as the Weierstrass preparation theorem.

@[protected]

A holomorphic function on a compact complex manifold is locally constant.

A holomorphic function on a compact connected complex manifold is constant.

A holomorphic function on a compact connected complex manifold is the constant function f ≡ v, for some value v.