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 #

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.

source

@[protected]

theorem mdifferentiable.is_locally_constant {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {F : Type u_2} [normed_add_comm_group F] [normed_space ℂ F] [strict_convex_space ℝ F] {M : Type u_3} [topological_space M] [compact_space M] [charted_space E M] [smooth_manifold_with_corners (model_with_corners_self ℂ E) M] {f : M → F} (hf : mdifferentiable (model_with_corners_self ℂ E) (model_with_corners_self ℂ F) f) :

is_locally_constant f

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

source

theorem mdifferentiable.apply_eq_of_compact_space {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {F : Type u_2} [normed_add_comm_group F] [normed_space ℂ F] [strict_convex_space ℝ F] {M : Type u_3} [topological_space M] [compact_space M] [charted_space E M] [smooth_manifold_with_corners (model_with_corners_self ℂ E) M] [preconnected_space M] {f : M → F} (hf : mdifferentiable (model_with_corners_self ℂ E) (model_with_corners_self ℂ F) f) (a b : M) :

f a = f b

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

source

theorem mdifferentiable.exists_eq_const_of_compact_space {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {F : Type u_2} [normed_add_comm_group F] [normed_space ℂ F] [strict_convex_space ℝ F] {M : Type u_3} [topological_space M] [compact_space M] [charted_space E M] [smooth_manifold_with_corners (model_with_corners_self ℂ E) M] [preconnected_space M] {f : M → F} (hf : mdifferentiable (model_with_corners_self ℂ E) (model_with_corners_self ℂ F) f) :

∃ (v : F), f = function.const M v

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