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 #

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:

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] [SmoothManifoldWithCorners I M] {f : MF} {c : M} (hd : ∀ᶠ (z : M) in nhds c, MDifferentiableAt I (modelWithCornersSelf F) 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] [SmoothManifoldWithCorners I M] {f : MF} {U : Set M} {c : M} (hd : MDifferentiableOn I (modelWithCornersSelf F) f U) (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] [SmoothManifoldWithCorners I M] [StrictConvexSpace F] {f : MF} {U : Set M} {c : M} (hd : MDifferentiableOn I (modelWithCornersSelf F) f U) (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] [SmoothManifoldWithCorners I M] {f : MF} {U : Set M} {a : M} {b : M} (hd : MDifferentiableOn I (modelWithCornersSelf F) f U) (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 #

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.

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] [SmoothManifoldWithCorners I M] [CompactSpace M] [PreconnectedSpace M] {f : MF} (hf : MDifferentiable I (modelWithCornersSelf F) f) (a : M) (b : M) :
f a = f b

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.