# mathlibdocumentation

geometry.manifold.complex

# 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.

## 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:

• the finite-dimensionality of the space of sections of a holomorphic vector bundle
• Siegel's theorem: for any n + 1 formal ratios g 0 / h 0, g 1 / h 1, .... g n / h n of sections of a fixed line bundle L over 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.

@[protected]
theorem mdifferentiable.is_locally_constant {E : Type u_1} [ E] {F : Type u_2} [ F] {M : Type u_3} [ M] {f : M → F} (hf : f) :

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

theorem mdifferentiable.apply_eq_of_compact_space {E : Type u_1} [ E] {F : Type u_2} [ F] {M : Type u_3} [ M] {f : M → F} (hf : f) (a b : M) :
f a = f b

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

theorem mdifferentiable.exists_eq_const_of_compact_space {E : Type u_1} [ E] {F : Type u_2} [ F] {M : Type u_3} [ M] {f : M → F} (hf : f) :
∃ (v : F), f =

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