/
manifold.lean
35 lines (26 loc) · 1.17 KB
/
manifold.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
/-
Copyright (c) 2022 Chris Birkbeck. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Birkbeck
-/
import analysis.complex.upper_half_plane.topology
import geometry.manifold.cont_mdiff_mfderiv
/-!
# Manifold structure on the upper half plane.
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
In this file we define the complex manifold structure on the upper half-plane.
-/
open_locale upper_half_plane manifold
namespace upper_half_plane
noncomputable instance : charted_space ℂ ℍ :=
upper_half_plane.open_embedding_coe.singleton_charted_space
instance : smooth_manifold_with_corners 𝓘(ℂ) ℍ :=
upper_half_plane.open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(ℂ)
/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
lemma smooth_coe : smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
λ x, cont_mdiff_at_ext_chart_at
/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
lemma mdifferentiable_coe : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
smooth_coe.mdifferentiable
end upper_half_plane