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} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {c : M} (hd : ∀ᶠ (z : M) in nhds c, MDiffAt f z) (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} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M} {c : M} (hd : MDiff[U] f) (hc : IsPreconnected U) (ho : IsOpen U) (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} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [StrictConvexSpace ℝ F] {f : M → F} {U : Set M} {c : M} (hd : MDiff[U] f) (hc : IsPreconnected U) (ho : IsOpen U) (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} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M} {a b : M} (hd : MDiff[U] f) (hpc : IsPreconnected U) (hc : IsCompact U) (ho : IsOpen U) (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

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} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] {f : M → F} (hf : MDiff f) : IsLocallyConstant f

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

theorem MDifferentiable.apply_eq_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] [PreconnectedSpace M] {f : M → F} (hf : MDiff 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_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] [PreconnectedSpace M] {f : M → F} (hf : MDiff 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.