Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Manifold structure on the upper half plane. #

In this file we define the complex manifold structure on the upper half-plane.

The inclusion map ℍ → ℂ is a map of C^n manifolds.

The inclusion map ℍ → ℂ is a differentiable map of manifolds.

Each element of GL(2, ℝ)⁺ defines a map of C ^ n manifolds ℍ → ℍ.

Each element of GL(2, ℝ)⁺ defines a complex-differentiable map ℍ → ℍ.