5.6. Surface.RealManifold🔗

Jacobians.Surface.RealManifold — source

realManifold_of_complex

A complex manifold is a real-C^∞ manifold. Holomorphic chart transitions are real-smooth, so the ℂ-atlas is a 𝓘(ℝ,ℂ)-smooth atlas. This is the foundational layer for real Dolbeault.

instance realManifold_of_complex {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] : IsManifold (𝓘(ℝ, ℂ)) (⊤ : ℕ∞) X