# Documentation

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

theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {f : MF} {c : M} (hd : ∀ᶠ (z : M) in nhds c, ) (hc : IsLocalMax (norm f) c) :
∀ᶠ (y : M) in nhds c, f y = f c

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 #

theorem MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {f : MF} {U : Set M} {c : M} (hd : ) (hc : ) (ho : ) (hcU : c U) (hm : IsMaxOn (norm f) U c) :
Set.EqOn (norm f) (Function.const M f c) 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.

theorem MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [] {f : MF} {U : Set M} {c : M} (hd : ) (hc : ) (ho : ) (hcU : c U) (hm : IsMaxOn (norm f) U c) :
Set.EqOn f (Function.const M (f c)) 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.

theorem MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {f : MF} {U : Set M} {a : M} {b : M} (hd : ) (hpc : ) (hc : ) (ho : ) (ha : a U) (hb : b U) :
f a = f b

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.

theorem MDifferentiable.isLocallyConstant {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [] {f : MF} (hf : ) :

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

theorem MDifferentiable.apply_eq_of_compactSpace {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [] {f : MF} (hf : ) (a : M) (b : M) :
f a = f b

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

theorem MDifferentiable.exists_eq_const_of_compactSpace {E : Type u_1} [] {F : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] [] {f : MF} (hf : ) :
v, f =

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