Complex manifolds are analytic

A complex manifold is a manifold modelled on a finite-dimensional complex normed space whose transition maps are holomorphic, that is C^1 over ℂ. By the several-variable Cauchy integral formula, a function of finitely many complex variables which is complex differentiable on an open set is analytic there (DifferentiableOn.analyticOnNhd_of_finiteDimensional). This file draws the manifold consequences of that fact, for a model without boundary.

• The C^n groupoids over ℂ coincide for all n ≠ 0, so a complex manifold of class C^1 is automatically of class C^n for every n, including n = ω, with the same maximal atlas.
• Restricting scalars, a complex manifold modelled on 𝓘(ℂ, E) is a real-analytic manifold modelled on 𝓘(ℝ, E), and each of its holomorphic charts is a real-analytic chart. This is the smooth structure underlying the real differential geometry of complex manifolds.
• A map between complex manifolds is holomorphic on an open set if and only if it is C^n there, for any n ≠ 0; holomorphy near a point is equivalent to being C^n at that point.

Main results

• TauCeti.contDiffGroupoid_le_of_ne_zero, TauCeti.contDiffGroupoid_eq_of_ne_zero: the C^m and C^n groupoids of a boundaryless model on a finite-dimensional complex space agree for m, n ≠ 0.
• IsManifold.of_ne_zero: a complex C^m manifold, m ≠ 0, is a complex C^n manifold for every n.
• IsManifold.maximalAtlas_eq_of_ne_zero: its maximal atlases for all orders n ≠ 0 agree.
• IsManifold.restrictScalars_of_ne_zero: a complex manifold modelled on 𝓘(ℂ, E) is a real C^n manifold modelled on 𝓘(ℝ, E) for every n, in particular a real-analytic one.
• IsManifold.maximalAtlas_subset_restrictScalars_of_ne_zero: its holomorphic charts belong to the real-analytic maximal atlas.
• MDifferentiableOn.contMDiffOn, MDifferentiable.contMDiff: a holomorphic map between complex manifolds is C^n for every n.
• TauCeti.contMDiffOn_iff_mdifferentiableOn, TauCeti.contMDiff_iff_mdifferentiable, TauCeti.contMDiffAt_iff_eventually_mdifferentiableAt: the corresponding characterizations of holomorphy.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, §2.2.

The groupoids and atlases of a complex manifold

theorem TauCeti.contDiffGroupoid_le_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {m n : WithTop ℕ∞} (hm : m ≠ 0) : contDiffGroupoid m I ≤ contDiffGroupoid n I

For a boundaryless model on a finite-dimensional complex space, the C^m groupoid is contained in the C^n groupoid for every n as soon as m ≠ 0.

theorem TauCeti.contDiffGroupoid_eq_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {m n : WithTop ℕ∞} (hm : m ≠ 0) (hn : n ≠ 0) : contDiffGroupoid m I = contDiffGroupoid n I

For a boundaryless model on a finite-dimensional complex space, the C^m and C^n groupoids agree whenever m and n are nonzero.

theorem IsManifold.of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {m : WithTop ℕ∞} (n : WithTop ℕ∞) (hm : m ≠ 0) (h : IsManifold I m M) : IsManifold I n M

A complex manifold of class C^m for some m ≠ 0, modelled without boundary on a finite-dimensional space, is a complex manifold of class C^n for every n, including n = ω.

theorem IsManifold.maximalAtlas_eq_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {m n : WithTop ℕ∞} (hm : m ≠ 0) (hn : n ≠ 0) : maximalAtlas I m M = maximalAtlas I n M

The maximal atlases of a complex manifold, modelled without boundary on a finite-dimensional space, agree for all nonzero orders of smoothness.

The underlying real-analytic manifold

theorem IsManifold.restrictScalars_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {m : WithTop ℕ∞} (n : WithTop ℕ∞) {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] (hm : m ≠ 0) (h : IsManifold (modelWithCornersSelf ℂ E) m M) : IsManifold (modelWithCornersSelf ℝ E) n M

A complex manifold is a real-analytic manifold. A complex manifold modelled on 𝓘(ℂ, E), of class C^m for some m ≠ 0 with E finite-dimensional, is with the same charts a real C^n manifold modelled on 𝓘(ℝ, E) for every n; for n = ω it is real-analytic.

theorem IsManifold.maximalAtlas_subset_restrictScalars_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {m : WithTop ℕ∞} (n : WithTop ℕ∞) {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] (hm : m ≠ 0) : maximalAtlas (modelWithCornersSelf ℂ E) m M ⊆ maximalAtlas (modelWithCornersSelf ℝ E) n M

Every holomorphic chart of a complex manifold modelled on 𝓘(ℂ, E), with E finite-dimensional, is a chart of the real C^n maximal atlas for every n; for n = ω it is a real-analytic chart.

Holomorphic maps

theorem MDifferentiableOn.contMDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} {s : Set M} (hf : MDiff[s] f) (hs : IsOpen s) : ContMDiffOn I I' n f s

A map between complex manifolds which is holomorphic on an open set is C^n on it for every n, including n = ω. The source is modelled without boundary on a finite-dimensional space; the target only needs a complete model space.

theorem MDifferentiable.contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} (hf : MDiff f) : ContMDiff I I' n f

A holomorphic map between complex manifolds is C^n for every n, including n = ω.

theorem TauCeti.contMDiffOn_iff_mdifferentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} {s : Set M} (hn : n ≠ 0) (hs : IsOpen s) : ContMDiffOn I I' n f s ↔ MDiff[s] f

On an open set, a map between complex manifolds is C^n, for any n ≠ 0, if and only if it is holomorphic.

theorem TauCeti.contMDiff_iff_mdifferentiable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} (hn : n ≠ 0) : ContMDiff I I' n f ↔ MDiff f

A map between complex manifolds is C^n, for any n ≠ 0, if and only if it is holomorphic.

theorem TauCeti.contMDiffAt_iff_eventually_mdifferentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} {x : M} (hn : n ≠ 0) : ContMDiffAt I I' n f x ↔ ∀ᶠ (y : M) in nhds x, MDiffAt f y

A map between complex manifolds is C^n at a point, for any n ≠ 0, if and only if it is holomorphic at every point of a neighbourhood. This is the manifold form of Complex.analyticAt_iff_eventually_differentiableAt.