Holomorphic functions on complex manifolds #
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 #
mdifferentiable.is_locally_constant: A complex-differentiable function on a compact complex manifold is locally constant.
mdifferentiable.exists_eq_const_of_compact_space: A complex-differentiable function on a compact preconnected complex manifold is constant.
There is a whole theory to develop here. Maybe a next step would be to develop a theory of holomorphic vector/line bundles, including:
- the finite-dimensionality of the space of sections of a holomorphic vector bundle
- Siegel's theorem: for any
n + 1formal ratios
g 0 / h 0,
g 1 / h 1, ....
g n / h nof sections of a fixed line bundle
Lover a complex
n-manifold, there exists a polynomial relationship
P (g 0 / h 0, g 1 / h 1, .... g n / h n) = 0
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.
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