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

: A complex-differentiable function on a compact complex manifold is locally constant.`MDifferentiable.exists_eq_const_of_compactSpace`

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

**Maximum modulus principle**: if `f : M → F`

is complex differentiable in a neighborhood of `c`

and the norm `‖f z‖`

has a local maximum at `c`

, then `‖f z‖`

is locally constant in a neighborhood
of `c`

. This is a manifold version of `Complex.norm_eventually_eq_of_isLocalMax`

.

### Functions holomorphic on a set #

**Maximum modulus principle** on a connected set. Let `U`

be a (pre)connected open set in a
complex normed space. Let `f : E → F`

be a function that is complex differentiable on `U`

. Suppose
that `‖f x‖`

takes its maximum value on `U`

at `c ∈ U`

. Then `‖f x‖ = ‖f c‖`

for all `x ∈ U`

.

**Maximum modulus principle** on a connected set. Let `U`

be a (pre)connected open set in a
complex normed space. Let `f : E → F`

be a function that is complex differentiable on `U`

. Suppose
that `‖f x‖`

takes its maximum value on `U`

at `c ∈ U`

. Then `f x = f c`

for all `x ∈ U`

.

TODO: change assumption from `IsMaxOn`

to `IsLocalMax`

.

If a function `f : M → F`

from a complex manifold to a complex normed space is holomorphic on a
(pre)connected compact open set, then it is a constant on this set.

### Functions holomorphic on the whole manifold #

Porting note: lemmas in this section were generalized from `𝓘(ℂ, E)`

to an unspecified boundaryless
model so that it works, e.g., on a product of two manifolds without a boundary. This can break
`apply MDifferentiable.apply_eq_of_compactSpace`

, use
`apply MDifferentiable.apply_eq_of_compactSpace (I := I)`

instead or dot notation on an existing
`MDifferentiable`

hypothesis.

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`

.